rw [ContinuousLinearMap.opNorm_le_iff (mul_nonneg (norm_nonneg x) (norm_nonneg (φ x)))]
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ‖(innerSL_smul φ) x‖ ≤ ‖x‖ * ‖φ x‖
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ∀ (x_1 : E), ‖((innerSL_smul φ) x) x_1‖ ≤ ‖x‖ * ‖φ x‖ * ‖x_1‖