𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ CompleteLattice.Independent V
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
⊢ CompleteLattice.Independent V
classical!
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ Function.Injective ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ CompleteLattice.Independent V
apply CompleteLattice.independent_of_dfinsupp_lsum_injective
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ LinearMap.ker (↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) = ⊥
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ Function.Injective ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i))
refine LinearMap.ker_eq_bot.mp ?_
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ ∀ (x : Π₀ (i : ι), { x // x ∈ V i }), x ∈ LinearMap.ker (↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) → x = 0
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ LinearMap.ker (↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) = ⊥
rw [Submodule.eq_bot_iff]
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : v ∈ LinearMap.ker (↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i))
⊢ v = 0
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
⊢ ∀ (x : Π₀ (i : ι), { x // x ∈ V i }), x ∈ LinearMap.ker (↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) → x = 0
intro v hv
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
⊢ v = 0
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : v ∈ LinearMap.ker (↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i))
⊢ v = 0
rw [LinearMap.mem_ker] at hv
case h.h.a
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
⊢ ↑(↑v i) = ↑(↑0 i)
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
⊢ v = 0
ext i
case h.h.a
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
⊢ inner ↑(↑v i) ↑(↑v i) = 0
case h.h.a
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
⊢ ↑(↑v i) = ↑(↑0 i)
suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
no goals
case h.h.a
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
⊢ inner ↑(↑v i) ↑(↑v i) = 0
calc
  ⟪(v i : E), v i⟫ = ⟪(v i : E), Dfinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
    simpa only [Dfinsupp.sumAddHom_apply, Dfinsupp.lsum_apply_apply] using
      (hV.inner_right_dfinsupp v i (v i)).symm
  _ = 0 := by simp only [hv, inner_zero_right]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
this : inner ↑(↑v i) ↑(↑v i) = 0
⊢ ↑(↑v i) = ↑(↑0 i)
simpa only [inner_self_eq_zero] using this
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
⊢ inner ↑(↑v i) ↑(↑v i) = inner (↑(↑v i)) (↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v)
simpa only [Dfinsupp.sumAddHom_apply, Dfinsupp.lsum_apply_apply] using
  (hV.inner_right_dfinsupp v i (v i)).symm
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3754417
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
G : ι → Type ?u.3754480
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V✝ : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ : OrthogonalFamily 𝕜 G V✝
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => Submodule.subtypeₗᵢ (V i)
em✝ : (a : Prop) → Decidable a
v : Π₀ (i : ι), { x // x ∈ V i }
hv : ↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v = 0
i : ι
⊢ inner (↑(↑v i)) (↑(↑(Dfinsupp.lsum ℕ) fun i => Submodule.subtype (V i)) v) = 0
simp only [hv, inner_zero_right]