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 
|- .x. = ( .r ` R )
Assertion mdetlap1 
|- ( ( R e. CRing /\ M e. B /\ I e. N ) -> ( D ` M ) = ( R gsum ( j e. N |-> ( ( I M j ) .x. ( 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 
 |-  .x. = ( .r ` R )
6 simp2 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> M e. B )
7 1 2 matmpo 
 |-  ( M e. B -> M = ( i e. N , j e. N |-> ( i M j ) ) )
8 eqid 
 |-  N = N
9 simpr 
 |-  ( ( T. /\ i = I ) -> i = I )
10 9 eqcomd 
 |-  ( ( T. /\ i = I ) -> I = i )
11 10 oveq1d 
 |-  ( ( T. /\ i = I ) -> ( I M j ) = ( i M j ) )
12 eqidd 
 |-  ( ( T. /\ -. i = I ) -> ( i M j ) = ( i M j ) )
13 11 12 ifeqda 
 |-  ( T. -> 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 e. N , j e. N |-> if ( i = I , ( I M j ) , ( i M j ) ) ) = ( i e. N , j e. N |-> ( i M j ) )
16 7 15 eqtr4di 
 |-  ( M e. B -> M = ( i e. N , j e. N |-> if ( i = I , ( I M j ) , ( i M j ) ) ) )
17 16 fveq2d 
 |-  ( M e. B -> ( D ` M ) = ( D ` ( i e. N , j e. N |-> if ( i = I , ( I M j ) , ( i M j ) ) ) ) )
18 6 17 syl 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> ( D ` M ) = ( D ` ( i e. N , j e. N |-> if ( i = I , ( I M j ) , ( i M j ) ) ) ) )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 simp1 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> R e. CRing )
21 simpl3 
 |-  ( ( ( R e. CRing /\ M e. B /\ I e. N ) /\ j e. N ) -> I e. N )
22 simpr 
 |-  ( ( ( R e. CRing /\ M e. B /\ I e. N ) /\ j e. N ) -> j e. N )
23 6 2 eleqtrdi 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> M e. ( Base ` A ) )
24 23 adantr 
 |-  ( ( ( R e. CRing /\ M e. B /\ I e. N ) /\ j e. N ) -> M e. ( Base ` A ) )
25 1 19 matecl 
 |-  ( ( I e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( I M j ) e. ( Base ` R ) )
26 21 22 24 25 syl3anc 
 |-  ( ( ( R e. CRing /\ M e. B /\ I e. N ) /\ j e. N ) -> ( I M j ) e. ( Base ` R ) )
27 simp3 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> I e. N )
28 1 4 2 3 5 19 6 20 26 27 madugsum 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> ( R gsum ( j e. N |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , ( I M j ) , ( i M j ) ) ) ) )
29 18 28 eqtr4d 
 |-  ( ( R e. CRing /\ M e. B /\ I e. N ) -> ( D ` M ) = ( R gsum ( j e. N |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) ) )