[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
⊢ Nondegenerate M
[PROOFSTEP]
intro v hv
[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
[PROOFSTEP]
ext i
[GOAL]
case h
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
i : m
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
specialize hv (M.cramer (Pi.single i 1))
[GOAL]
case h
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
refine' (mul_eq_zero.mp _).resolve_right hM
[GOAL]
case h
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = 0
[PROOFSTEP]
convert hv
[GOAL]
case h.e'_2
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1))
[PROOFSTEP]
simp only [mulVec_cramer M (Pi.single i 1), dotProduct, Pi.smul_apply, smul_eq_mul]
[GOAL]
case h.e'_2
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = Finset.sum Finset.univ fun x => v x * (det M * Pi.single i 1 x)
[PROOFSTEP]
rw [Finset.sum_eq_single i, Pi.single_eq_same, mul_one]
[GOAL]
case h.e'_2.h₀
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ i → v b * (det M * Pi.single i 1 b) = 0
[PROOFSTEP]
intro j _ hj
[GOAL]
case h.e'_2.h₀
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
j : m
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ v j * (det M * Pi.single i 1 j) = 0
[PROOFSTEP]
simp [hj]
[GOAL]
case h.e'_2.h₁
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ¬i ∈ Finset.univ → v i * (det M * Pi.single i 1 i) = 0
[PROOFSTEP]
intros
[GOAL]
case h.e'_2.h₁
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
[PROOFSTEP]
have := Finset.mem_univ i
[GOAL]
case h.e'_2.h₁
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
[PROOFSTEP]
contradiction
[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : vecMul v M = 0
w : m → A
⊢ v ⬝ᵥ mulVec M w = 0
[PROOFSTEP]
rw [dotProduct_mulVec, hv, zero_dotProduct]
[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : mulVec M v = 0
⊢ det Mᵀ ≠ 0
[PROOFSTEP]
rwa [det_transpose]
