[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let A := toMatrix b b f
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let b' := chooseBasis R M
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let ι' := ChooseBasisIndex R M
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let A' := toMatrix b' b' f
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let e := Basis.indexEquiv b b'
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ := reindexLinearEquiv R R e e
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ₁ := reindexLinearEquiv R R e (Equiv.refl ι')
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ₂ := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ₃ := reindexLinearEquiv R R (Equiv.refl ι') e
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let P := b.toMatrix b'
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let Q := b'.toMatrix b
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
have hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1 := by
  rw [RingHom.mapMatrix_apply, RingHom.mapMatrix_apply, ← Matrix.map_mul, reindexLinearEquiv_mul R R,
    Basis.toMatrix_mul_toMatrix_flip, reindexLinearEquiv_one, ← RingHom.mapMatrix_apply, RingHom.map_one]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
[PROOFSTEP]
rw [RingHom.mapMatrix_apply, RingHom.mapMatrix_apply, ← Matrix.map_mul, reindexLinearEquiv_mul R R,
  Basis.toMatrix_mul_toMatrix_flip, reindexLinearEquiv_one, ← RingHom.mapMatrix_apply, RingHom.map_one]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
calc
  A.charpoly = (reindex e e A).charpoly := (charpoly_reindex _ _).symm
  _ = det (scalar ι' X - C.mapMatrix (φ A)) := rfl
  _ = det (scalar ι' X - C.mapMatrix (φ (P * A' * Q))) := by
    rw [basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix]
  _ = det (scalar ι' X - C.mapMatrix (φ₁ P * φ₂ A' * φ₃ Q)) := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
  _ = det (scalar ι' X - C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)) := by simp
  _ =
      det
        (scalar ι' X * C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) -
          C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)) :=
    by rw [Matrix.mul_assoc ((scalar ι') X), hPQ, Matrix.mul_one]
  _ =
      det
        (C.mapMatrix (φ₁ P) * scalar ι' X * C.mapMatrix (φ₃ Q) -
          C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)) :=
    by simp
  _ = det (C.mapMatrix (φ₁ P) * (scalar ι' X - C.mapMatrix A') * C.mapMatrix (φ₃ Q)) := by
    rw [← Matrix.sub_mul, ← Matrix.mul_sub]
  _ = det (C.mapMatrix (φ₁ P)) * det (scalar ι' X - C.mapMatrix A') * det (C.mapMatrix (φ₃ Q)) := by
    rw [det_mul, det_mul]
  _ = det (C.mapMatrix (φ₁ P)) * det (C.mapMatrix (φ₃ Q)) * det (scalar ι' X - C.mapMatrix A') := by ring
  _ = det (scalar ι' X - C.mapMatrix A') := by rw [← det_mul, hPQ, det_one, one_mul]
  _ = f.charpoly := rfl
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ A)) = det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ (P * A' * Q)))
[PROOFSTEP]
rw [basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ (P * A' * Q))) =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P * ↑φ₂ A' * ↑φ₃ Q))
[PROOFSTEP]
rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P * ↑φ₂ A' * ↑φ₃ Q)) =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
simp
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det
      (↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
rw [Matrix.mul_assoc ((scalar ι') X), hPQ, Matrix.mul_one]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det
      (↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det
      (↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
simp
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det
      (↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P) * (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
rw [← Matrix.sub_mul, ← Matrix.mul_sub]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P) * (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') *
      det (↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
rw [det_mul, det_mul]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') *
      det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) *
      det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A')
[PROOFSTEP]
ring
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) *
      det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A')
[PROOFSTEP]
rw [← det_mul, hPQ, det_one, one_mul]
