ι : Type u_1
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
W₀ : Π₀ (i : ι), G i
this :
  ↑(OrthogonalFamily.linearIsometry hV) (∑ i in Dfinsupp.support W₀, lp.single 2 i (↑W₀ i)) =
    ∑ i in Dfinsupp.support W₀, ↑(OrthogonalFamily.linearIsometry hV) (lp.single 2 i (↑W₀ i))
⊢ ↑(OrthogonalFamily.linearIsometry hV) (Dfinsupp.sum W₀ (lp.single 2)) = Dfinsupp.sum W₀ fun i => ↑(V i)
ι : Type u_1
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(OrthogonalFamily.linearIsometry hV) (Dfinsupp.sum W₀ (lp.single 2)) = Dfinsupp.sum W₀ fun i => ↑(V i)
have :
  hV.linearIsometry (∑ i in W₀.support, lp.single 2 i (W₀ i)) =
    ∑ i in W₀.support, hV.linearIsometry (lp.single 2 i (W₀ i)) :=
  hV.linearIsometry.toLinearMap.map_sum
no goals
ι : Type u_1
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
W₀ : Π₀ (i : ι), G i
this :
  ↑(OrthogonalFamily.linearIsometry hV) (∑ i in Dfinsupp.support W₀, lp.single 2 i (↑W₀ i)) =
    ∑ i in Dfinsupp.support W₀, ↑(OrthogonalFamily.linearIsometry hV) (lp.single 2 i (↑W₀ i))
⊢ ↑(OrthogonalFamily.linearIsometry hV) (Dfinsupp.sum W₀ (lp.single 2)) = Dfinsupp.sum W₀ fun i => ↑(V i)
simp (config := { contextual := true }) [Dfinsupp.sum, this]