𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ↑(toDualMap 𝕜 E) x = ↑(toDualMap 𝕜 E) y
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ x = y
apply (toDualMap 𝕜 E).map_eq_iff.mp
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ∀ (i : ι), ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ↑(toDualMap 𝕜 E) x = ↑(toDualMap 𝕜 E) y
refine' (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (Basis.ext b _)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ∀ (i : ι), ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
intro i
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑(↑(toDualMap 𝕜 E) y) (↑b i)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
simp only [ContinuousLinearMap.coe_coe]
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ inner x (↑b i) = inner y (↑b i)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑(↑(toDualMap 𝕜 E) y) (↑b i)
rw [toDualMap_apply, toDualMap_apply]
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = inner y (↑b i)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ inner x (↑b i) = inner y (↑b i)
rw [← inner_conj_symm]
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = ↑(starRingEnd 𝕜) (inner (↑b i) y)
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = inner y (↑b i)
conv_rhs => rw [← inner_conj_symm]
no goals
𝕜 : Type u_2
E : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_1
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = ↑(starRingEnd 𝕜) (inner (↑b i) y)
exact congr_arg conj (h i)