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 9 24 syl 
 |-  ( ph -> R e. Ring )
26 6 zrhrhm 
 |-  ( R e. Ring -> Z e. ( ZZring RingHom R ) )
27 zringbas 
 |-  ZZ = ( Base ` ZZring )
28 27 22 rhmf 
 |-  ( Z e. ( ZZring RingHom R ) -> Z : ZZ --> ( Base ` R ) )
29 25 26 28 3syl 
 |-  ( ph -> Z : ZZ --> ( Base ` R ) )
30 29 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> Z : ZZ --> ( Base ` R ) )
31 1zzd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> 1 e. ZZ )
32 31 znegcld 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> -u 1 e. ZZ )
33 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
34 33 17 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> I e. NN )
35 33 18 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN )
36 34 35 nnaddcld 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I + j ) e. NN )
37 36 nnnn0d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I + j ) e. NN0 )
38 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ ( I + j ) e. NN0 ) -> ( -u 1 ^ ( I + j ) ) e. ZZ )
39 32 37 38 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( -u 1 ^ ( I + j ) ) e. ZZ )
40 30 39 ffvelrnd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( Z ` ( -u 1 ^ ( I + j ) ) ) e. ( Base ` R ) )
41 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 ) ) )
42 16 23 40 41 syl3anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( I M j ) .x. ( Z ` ( -u 1 ^ ( I + j ) ) ) ) = ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( I M j ) ) )
43 42 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 ) ) ) )
44 16 24 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> R e. Ring )
45 eqid 
 |-  ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )
46 eqid 
 |-  ( I ( subMat1 ` M ) j ) = ( I ( subMat1 ` M ) j )
47 2 1 45 46 15 17 18 19 smatcl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( I ( subMat1 ` M ) j ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
48 eqid 
 |-  ( ( 1 ... ( N - 1 ) ) Mat R ) = ( ( 1 ... ( N - 1 ) ) Mat R )
49 7 48 45 22 mdetcl 
 |-  ( ( R e. CRing /\ ( I ( subMat1 ` M ) j ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) ) -> ( E ` ( I ( subMat1 ` M ) j ) ) e. ( Base ` R ) )
50 16 47 49 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( E ` ( I ( subMat1 ` M ) j ) ) e. ( Base ` R ) )
51 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 ) ) ) ) )
52 44 23 40 50 51 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 ) ) ) ) )
53 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 ) ) ) ) )
54 44 40 23 50 53 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 ) ) ) ) )
55 43 52 54 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 ) ) ) ) )
56 21 55 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 ) ) ) ) )
57 56 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 ) ) ) ) ) )
58 57 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 ) ) ) ) ) ) )
59 14 58 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 ) ) ) ) ) ) )