𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ‖↑u e‖₊ ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
⊢ ‖↑u e‖₊ ≤ Fintype.card ι • ‖↑(equivFunL v)‖₊ * M * ‖e‖₊
set φ := v.equivFunL.toContinuousLinearMap
no goals
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ‖↑u e‖₊ ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
calc
  ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
  _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp [u.map_sum, LinearMap.map_smul]
  _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := (nnnorm_sum_le _ _)
  _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
  _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
  _ = (∑ i, ‖v.equivFun e i‖₊) * M := Finset.sum_mul.symm
  _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
    gcongr
    calc
      (∑ i, ‖v.equivFun e i‖₊) ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_of_le_right (φ.le_op_nnnorm e) _
  _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
no goals
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ‖↑u e‖₊ = ‖↑u (∑ i : ι, ↑(equivFun v) e i • ↑v i)‖₊
rw [v.sum_equivFun]
no goals
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ‖↑u (∑ i : ι, ↑(equivFun v) e i • ↑v i)‖₊ = ‖∑ i : ι, ↑(equivFun v) e i • ↑u (↑v i)‖₊
simp [u.map_sum, LinearMap.map_smul]
no goals
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ∑ i : ι, ‖↑(equivFun v) e i • ↑u (↑v i)‖₊ = ∑ i : ι, ‖↑(equivFun v) e i‖₊ * ‖↑u (↑v i)‖₊
simp only [nnnorm_smul]
case h.bc
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
i✝ : ι
a✝ : i✝ ∈ Finset.univ
⊢ ‖↑u (↑v i✝)‖₊ ≤ M
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ∑ i : ι, ‖↑(equivFun v) e i‖₊ * ‖↑u (↑v i)‖₊ ≤ ∑ i : ι, ‖↑(equivFun v) e i‖₊ * M
gcongr
no goals
case h.bc
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
i✝ : ι
a✝ : i✝ ∈ Finset.univ
⊢ ‖↑u (↑v i✝)‖₊ ≤ M
apply hu
case bc
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ∑ i : ι, ‖↑(equivFun v) e i‖₊ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊)
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ (∑ i : ι, ‖↑(equivFun v) e i‖₊) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M
gcongr
no goals
case bc
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ ∑ i : ι, ‖↑(equivFun v) e i‖₊ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊)
calc
  (∑ i, ‖v.equivFun e i‖₊) ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
  _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_of_le_right (φ.le_op_nnnorm e) _
no goals
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑(equivFunL v)
⊢ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
simp only [smul_mul_assoc, mul_right_comm]