𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (l : ι →₀ 𝕜), ↑(Finsupp.total ι E 𝕜 v) l = 0 → l = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
⊢ LinearIndependent 𝕜 v
rw [linearIndependent_iff]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
⊢ l = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (l : ι →₀ 𝕜), ↑(Finsupp.total ι E 𝕜 v) l = 0 → l = 0
intro l hl
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
i : ι
⊢ ↑l i = ↑0 i
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
⊢ l = 0
ext i
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
i : ι
key : inner (v i) (↑(Finsupp.total ι E 𝕜 v) l) = inner (v i) 0
⊢ ↑l i = ↑0 i
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
i : ι
⊢ ↑l i = ↑0 i
have key : ⟪v i, Finsupp.total ι E 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]
no goals
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
i : ι
key : inner (v i) (↑(Finsupp.total ι E 𝕜 v) l) = inner (v i) 0
⊢ ↑l i = ↑0 i
simpa only [hv.inner_right_finsupp, inner_zero_right] using key
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2133622
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : ↑(Finsupp.total ι E 𝕜 v) l = 0
i : ι
⊢ inner (v i) (↑(Finsupp.total ι E 𝕜 v) l) = inner (v i) 0
rw [hl]