Metamath Proof Explorer

Theorem mdetlap1

Description: A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020)

Ref Expression
Hypotheses mdetlap1.a ⊢ A = N Mat R
mdetlap1.b ⊢ B = Base A
mdetlap1.d ⊢ D = N maDet R
mdetlap1.k ⊢ K = N maAdju R
mdetlap1.t ⊢ · ˙ = ⋅ R
Assertion mdetlap1 ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → D ⁡ M = ∑ R j ∈ N I M j · ˙ j K ⁡ M I

Proof

Step Hyp Ref Expression
1 mdetlap1.a ⊢ A = N Mat R
2 mdetlap1.b ⊢ B = Base A
3 mdetlap1.d ⊢ D = N maDet R
4 mdetlap1.k ⊢ K = N maAdju R
5 mdetlap1.t ⊢ · ˙ = ⋅ R
6 simp2 ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → M ∈ B
7 1 2 matmpo ⊢ M ∈ B → M = i ∈ N , j ∈ N ⟼ i M j
8 eqid ⊢ N = N
9 simpr ⊢ ⊤ ∧ i = I → i = I
10 9 eqcomd ⊢ ⊤ ∧ i = I → I = i
11 10 oveq1d ⊢ ⊤ ∧ i = I → I M j = i M j
12 eqidd ⊢ ⊤ ∧ ¬ i = I → i M j = i M j
13 11 12 ifeqda ⊢ ⊤ → if i = I I M j i M j = i M j
14 13 mptru ⊢ if i = I I M j i M j = i M j
15 8 8 14 mpoeq123i ⊢ i ∈ N , j ∈ N ⟼ if i = I I M j i M j = i ∈ N , j ∈ N ⟼ i M j
16 7 15 eqtr4di ⊢ M ∈ B → M = i ∈ N , j ∈ N ⟼ if i = I I M j i M j
17 16 fveq2d ⊢ M ∈ B → D ⁡ M = D ⁡ i ∈ N , j ∈ N ⟼ if i = I I M j i M j
18 6 17 syl ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → D ⁡ M = D ⁡ i ∈ N , j ∈ N ⟼ if i = I I M j i M j
19 eqid ⊢ Base R = Base R
20 simp1 ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → R ∈ CRing
21 simpl3 ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N ∧ j ∈ N → I ∈ N
22 simpr ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N ∧ j ∈ N → j ∈ N
23 6 2 eleqtrdi ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → M ∈ Base A
24 23 adantr ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N ∧ j ∈ N → M ∈ Base A
25 1 19 matecl ⊢ I ∈ N ∧ j ∈ N ∧ M ∈ Base A → I M j ∈ Base R
26 21 22 24 25 syl3anc ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N ∧ j ∈ N → I M j ∈ Base R
27 simp3 ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → I ∈ N
28 1 4 2 3 5 19 6 20 26 27 madugsum ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → ∑ R j ∈ N I M j · ˙ j K ⁡ M I = D ⁡ i ∈ N , j ∈ N ⟼ if i = I I M j i M j
29 18 28 eqtr4d ⊢ R ∈ CRing ∧ M ∈ B ∧ I ∈ N → D ⁡ M = ∑ R j ∈ N I M j · ˙ j K ⁡ M I