[GOAL]
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
⊢ ↑(toMatrix (Basis.dualBasis B₂) (Basis.dualBasis B₁)) (↑Module.Dual.transpose u) = (↑(toMatrix B₁ B₂) u)ᵀ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
i : ι₁
j : ι₂
⊢ ↑(toMatrix (Basis.dualBasis B₂) (Basis.dualBasis B₁)) (↑Module.Dual.transpose u) i j = (↑(toMatrix B₁ B₂) u)ᵀ i j
[PROOFSTEP]
simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr, B₂.dualBasis_apply,
  Matrix.transpose_apply, LinearMap.comp_apply]
[GOAL]
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ = ↑Module.Dual.transpose (↑(toLin B₂ B₁) M)
[PROOFSTEP]
apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective
[GOAL]
case a
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂))
      (↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ) =
    ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂)) (↑Module.Dual.transpose (↑(toLin B₂ B₁) M))
[PROOFSTEP]
rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]
