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=NMatR
mdetlap1.b ⊢B=BaseA
mdetlap1.d ⊢D=NmaDetR
mdetlap1.k ⊢K=NmaAdjuR
mdetlap1.t ⊢·˙=⋅R
Assertion mdetlap1 ⊢R∈CRing∧M∈B∧I∈N→D⁡M=∑Rj∈NIMj·˙jK⁡MI

Proof

Step Hyp Ref Expression
1 mdetlap1.a ⊢A=NMatR
2 mdetlap1.b ⊢B=BaseA
3 mdetlap1.d ⊢D=NmaDetR
4 mdetlap1.k ⊢K=NmaAdjuR
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⟼iMj
8 eqid ⊢N=N
9 simpr ⊢⊤∧i=I→i=I
10 9 eqcomd ⊢⊤∧i=I→I=i
11 10 oveq1d ⊢⊤∧i=I→IMj=iMj
12 eqidd ⊢⊤∧¬i=I→iMj=iMj
13 11 12 ifeqda ⊢⊤→ifi=IIMjiMj=iMj
14 13 mptru ⊢ifi=IIMjiMj=iMj
15 8 8 14 mpoeq123i ⊢i∈N,j∈N⟼ifi=IIMjiMj=i∈N,j∈N⟼iMj
16 7 15 eqtr4di ⊢M∈B→M=i∈N,j∈N⟼ifi=IIMjiMj
17 16 fveq2d ⊢M∈B→D⁡M=D⁡i∈N,j∈N⟼ifi=IIMjiMj
18 6 17 syl ⊢R∈CRing∧M∈B∧I∈N→D⁡M=D⁡i∈N,j∈N⟼ifi=IIMjiMj
19 eqid ⊢BaseR=BaseR
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∈BaseA
24 23 adantr ⊢R∈CRing∧M∈B∧I∈N∧j∈N→M∈BaseA
25 1 19 matecl ⊢I∈N∧j∈N∧M∈BaseA→IMj∈BaseR
26 21 22 24 25 syl3anc ⊢R∈CRing∧M∈B∧I∈N∧j∈N→IMj∈BaseR
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→∑Rj∈NIMj·˙jK⁡MI=D⁡i∈N,j∈N⟼ifi=IIMjiMj
29 18 28 eqtr4d ⊢R∈CRing∧M∈B∧I∈N→D⁡M=∑Rj∈NIMj·˙jK⁡MI