Metamath Proof Explorer

Theorem mdetlap

Description: Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Hypotheses madjusmdet.b 
|- B = ( Base ` A )
madjusmdet.a 
|- A = ( ( 1 ... N ) Mat R )
madjusmdet.d 
|- D = ( ( 1 ... N ) maDet R )
madjusmdet.k 
|- K = ( ( 1 ... N ) maAdju R )
madjusmdet.t 
|- .x. = ( .r ` R )
madjusmdet.z 
|- Z = ( ZRHom ` R )
madjusmdet.e 
|- E = ( ( 1 ... ( N - 1 ) ) maDet R )
madjusmdet.n 
|- ( ph -> N e. NN )
madjusmdet.r 
|- ( ph -> R e. CRing )
madjusmdet.i 
|- ( ph -> I e. ( 1 ... N ) )
madjusmdet.j 
|- ( ph -> J e. ( 1 ... N ) )
madjusmdet.m 
|- ( ph -> M e. B )
Assertion mdetlap 
|- ( ph -> ( D ` M ) = ( R gsum ( j e. ( 1 ... N ) |-> ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 madjusmdet.b 
 |-  B = ( Base ` A )
2 madjusmdet.a 
 |-  A = ( ( 1 ... N ) Mat R )
3 madjusmdet.d 
 |-  D = ( ( 1 ... N ) maDet R )
4 madjusmdet.k 
 |-  K = ( ( 1 ... N ) maAdju R )
5 madjusmdet.t 
 |-  .x. = ( .r ` R )
6 madjusmdet.z 
 |-  Z = ( ZRHom ` R )
7 madjusmdet.e 
 |-  E = ( ( 1 ... ( N - 1 ) ) maDet R )
8 madjusmdet.n 
 |-  ( ph -> N e. NN )
9 madjusmdet.r 
 |-  ( ph -> R e. CRing )
10 madjusmdet.i 
 |-  ( ph -> I e. ( 1 ... N ) )
11 madjusmdet.j 
 |-  ( ph -> J e. ( 1 ... N ) )
12 madjusmdet.m 
 |-  ( ph -> M e. B )
13 2 1 3 4 5 mdetlap1 
 |-  ( ( R e. CRing /\ M e. B /\ I e. ( 1 ... N ) ) -> ( D ` M ) = ( R gsum ( j e. ( 1 ... N ) |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) ) )
14 9 12 10 13 syl3anc 
 |-  ( ph -> ( D ` M ) = ( R gsum ( j e. ( 1 ... N ) |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) ) )
15 8 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N e. NN )
16 9 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> R e. CRing )
17 10 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> I e. ( 1 ... N ) )
18 simpr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
19 12 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> M e. B )
20 1 2 3 4 5 6 7 15 16 17 18 19 madjusmdet 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) )
21 20 oveq2d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( I M j ) .x. ( j ( K ` M ) I ) ) = ( ( I M j ) .x. ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
22 eqid 
 |-  ( Base ` R ) = ( Base ` R )
23 2 22 1 17 18 19 matecld 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I M j ) e. ( Base ` R ) )
24 crngring 
 |-  ( R e. CRing -> R e. Ring )
25 6 zrhrhm 
 |-  ( R e. Ring -> Z e. ( ZZring RingHom R ) )
26 zringbas 
 |-  ZZ = ( Base ` ZZring )
27 26 22 rhmf 
 |-  ( Z e. ( ZZring RingHom R ) -> Z : ZZ --> ( Base ` R ) )
28 9 24 25 27 4syl 
 |-  ( ph -> Z : ZZ --> ( Base ` R ) )
29 28 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> Z : ZZ --> ( Base ` R ) )
30 1zzd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> 1 e. ZZ )
31 30 znegcld 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> -u 1 e. ZZ )
32 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
33 32 17 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> I e. NN )
34 32 18 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN )
35 33 34 nnaddcld 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I + j ) e. NN )
36 35 nnnn0d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I + j ) e. NN0 )
37 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ ( I + j ) e. NN0 ) -> ( -u 1 ^ ( I + j ) ) e. ZZ )
38 31 36 37 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( -u 1 ^ ( I + j ) ) e. ZZ )
39 29 38 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( Z ` ( -u 1 ^ ( I + j ) ) ) e. ( Base ` R ) )
40 22 5 crngcom 
 |-  ( ( R e. CRing /\ ( I M j ) e. ( Base ` R ) /\ ( Z ` ( -u 1 ^ ( I + j ) ) ) e. ( Base ` R ) ) -> ( ( I M j ) .x. ( Z ` ( -u 1 ^ ( I + j ) ) ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( I M j ) ) )
41 16 23 39 40 syl3anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( I M j ) .x. ( Z ` ( -u 1 ^ ( I + j ) ) ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( I M j ) ) )
42 41 oveq1d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( ( I M j ) .x. ( Z ` ( -u 1 ^ ( I + j ) ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) = ( ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( I M j ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) )
43 16 24 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> R e. Ring )
44 eqid 
 |-  ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )
45 eqid 
 |-  ( I ( subMat1 ` M ) j ) = ( I ( subMat1 ` M ) j )
46 2 1 44 45 15 17 18 19 smatcl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I ( subMat1 ` M ) j ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
47 eqid 
 |-  ( ( 1 ... ( N - 1 ) ) Mat R ) = ( ( 1 ... ( N - 1 ) ) Mat R )
48 7 47 44 22 mdetcl 
 |-  ( ( R e. CRing /\ ( I ( subMat1 ` M ) j ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) ) -> ( E ` ( I ( subMat1 ` M ) j ) ) e. ( Base ` R ) )
49 16 46 48 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( E ` ( I ( subMat1 ` M ) j ) ) e. ( Base ` R ) )
50 22 5 ringass 
 |-  ( ( R e. Ring /\ ( ( I M j ) e. ( Base ` R ) /\ ( Z ` ( -u 1 ^ ( I + j ) ) ) e. ( Base ` R ) /\ ( E ` ( I ( subMat1 ` M ) j ) ) e. ( Base ` R ) ) ) -> ( ( ( I M j ) .x. ( Z ` ( -u 1 ^ ( I + j ) ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) = ( ( I M j ) .x. ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
51 43 23 39 49 50 syl13anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( ( I M j ) .x. ( Z ` ( -u 1 ^ ( I + j ) ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) = ( ( I M j ) .x. ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
52 22 5 ringass 
 |-  ( ( R e. Ring /\ ( ( Z ` ( -u 1 ^ ( I + j ) ) ) e. ( Base ` R ) /\ ( I M j ) e. ( Base ` R ) /\ ( E ` ( I ( subMat1 ` M ) j ) ) e. ( Base ` R ) ) ) -> ( ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( I M j ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
53 43 39 23 49 52 syl13anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( I M j ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
54 42 51 53 3eqtr3d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( I M j ) .x. ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
55 21 54 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( I M j ) .x. ( j ( K ` M ) I ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) )
56 55 mpteq2dva 
 |-  ( ph -> ( j e. ( 1 ... N ) |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) = ( j e. ( 1 ... N ) |-> ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) ) )
57 56 oveq2d 
 |-  ( ph -> ( R gsum ( j e. ( 1 ... N ) |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) ) = ( R gsum ( j e. ( 1 ... N ) |-> ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) ) ) )
58 14 57 eqtrd 
 |-  ( ph -> ( D ` M ) = ( R gsum ( j e. ( 1 ... N ) |-> ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I ( subMat1 ` M ) j ) ) ) ) ) ) )