ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(↑(linearIsometryEquiv hV) (↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) (Dfinsupp.sum W₀ (lp.single 2)))) =
    ↑W₀
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(↑(linearIsometryEquiv hV) (Dfinsupp.sum W₀ fun i => ↑(V i))) = ↑W₀
rw [← hV.linearIsometryEquiv_symm_apply_dfinsupp_sum_single]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(Dfinsupp.sum W₀ (lp.single 2)) = ↑W₀
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(↑(linearIsometryEquiv hV) (↑(LinearIsometryEquiv.symm (linearIsometryEquiv hV)) (Dfinsupp.sum W₀ (lp.single 2)))) =
    ↑W₀
rw [LinearIsometryEquiv.apply_symm_apply]
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
i : ι
⊢ ↑(Dfinsupp.sum W₀ (lp.single 2)) i = ↑W₀ i
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(Dfinsupp.sum W₀ (lp.single 2)) = ↑W₀
ext i
no goals
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
i : ι
⊢ ↑(Dfinsupp.sum W₀ (lp.single 2)) i = ↑W₀ i
simp (config := { contextual := true }) [Dfinsupp.sum, lp.single_apply]