ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ↑(↑(innerSL 𝕜) x) (∑ i : ι, ↑b.repr y i • ↑b i) = ↑(↑(innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (↑b i) * inner (↑b i) y = inner x y
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
⊢ ∑ i : ι, inner x (↑b i) * inner (↑b i) y = inner x y
have := congr_arg (innerSL 𝕜 x) (b.sum_repr y)
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ↑(↑(innerSL 𝕜) x) (↑b.repr y x_1 • ↑b x_1) = ↑(↑(innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (↑b i) * inner (↑b i) y = inner x y
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ↑(↑(innerSL 𝕜) x) (∑ i : ι, ↑b.repr y i • ↑b i) = ↑(↑(innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (↑b i) * inner (↑b i) y = inner x y
rw [map_sum] at this
case h.e'_2.a
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ↑(↑(innerSL 𝕜) x) (↑b.repr y x_1 • ↑b x_1) = ↑(↑(innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner x (↑b x✝) * inner (↑b x✝) y = ↑(↑(innerSL 𝕜) x) (↑b.repr y x✝ • ↑b x✝)
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ↑(↑(innerSL 𝕜) x) (↑b.repr y x_1 • ↑b x_1) = ↑(↑(innerSL 𝕜) x) y
⊢ ∑ i : ι, inner x (↑b i) * inner (↑b i) y = inner x y
convert this
case h.e'_2.a
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ↑(↑(innerSL 𝕜) x) (↑b.repr y x_1 • ↑b x_1) = ↑(↑(innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (↑b x✝) y * inner x (↑b x✝) = inner (↑b x✝) y • ↑(↑(innerSL 𝕜) x) (↑b x✝)
case h.e'_2.a
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ↑(↑(innerSL 𝕜) x) (↑b.repr y x_1 • ↑b x_1) = ↑(↑(innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner x (↑b x✝) * inner (↑b x✝) y = ↑(↑(innerSL 𝕜) x) (↑b.repr y x✝ • ↑b x✝)
rw [SMulHomClass.map_smul, b.repr_apply_apply, mul_comm]
no goals
case h.e'_2.a
ι : Type u_1
ι' : Type ?u.827323
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.827352
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.827370
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.827390
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1 : ι, ↑(↑(innerSL 𝕜) x) (↑b.repr y x_1 • ↑b x_1) = ↑(↑(innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (↑b x✝) y * inner x (↑b x✝) = inner (↑b x✝) y • ↑(↑(innerSL 𝕜) x) (↑b x✝)
simp only [innerSL_apply, smul_eq_mul]