Metamath Proof Explorer

Theorem mdetdiag

Description: The determinant of a diagonal matrix is the product of the entries in the diagonal. (Contributed by AV, 17-Aug-2019)

Ref Expression
Hypotheses mdetdiag.d 
|- D = ( N maDet R )
mdetdiag.a 
|- A = ( N Mat R )
mdetdiag.b 
|- B = ( Base ` A )
mdetdiag.g 
|- G = ( mulGrp ` R )
mdetdiag.0 
|- .0. = ( 0g ` R )
Assertion mdetdiag 
|- ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> ( D ` M ) = ( G gsum ( k e. N |-> ( k M k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetdiag.d 
 |-  D = ( N maDet R )
2 mdetdiag.a 
 |-  A = ( N Mat R )
3 mdetdiag.b 
 |-  B = ( Base ` A )
4 mdetdiag.g 
 |-  G = ( mulGrp ` R )
5 mdetdiag.0 
 |-  .0. = ( 0g ` R )
6 simpl3 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> M e. B )
7 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
8 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
9 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 1 2 3 7 8 9 10 4 mdetleib 
 |-  ( M e. B -> ( D ` M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) ) ) )
12 6 11 syl 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( D ` M ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) ) ) )
13 simpl1 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> R e. CRing )
14 13 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ p = ( _I |` N ) ) -> R e. CRing )
15 6 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ p = ( _I |` N ) ) -> M e. B )
16 simpr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ p = ( _I |` N ) ) -> p = ( _I |` N ) )
17 2 3 4 8 9 10 madetsumid 
 |-  ( ( R e. CRing /\ M e. B /\ p = ( _I |` N ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = ( G gsum ( k e. N |-> ( k M k ) ) ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ p = ( _I |` N ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = ( G gsum ( k e. N |-> ( k M k ) ) ) )
19 iftrue 
 |-  ( p = ( _I |` N ) -> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) = ( G gsum ( k e. N |-> ( k M k ) ) ) )
20 19 eqcomd 
 |-  ( p = ( _I |` N ) -> ( G gsum ( k e. N |-> ( k M k ) ) ) = if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
21 20 adantl 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ p = ( _I |` N ) ) -> ( G gsum ( k e. N |-> ( k M k ) ) ) = if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
22 18 21 eqtrd 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ p = ( _I |` N ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
23 simplll 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> ( R e. CRing /\ N e. Fin /\ M e. B ) )
24 simpr 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) )
25 24 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) )
26 simpr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> p e. ( Base ` ( SymGrp ` N ) ) )
27 neqne 
 |-  ( -. p = ( _I |` N ) -> p =/= ( _I |` N ) )
28 26 27 anim12i 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> ( p e. ( Base ` ( SymGrp ` N ) ) /\ p =/= ( _I |` N ) ) )
29 1 2 3 4 5 7 8 9 10 mdetdiaglem 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( p e. ( Base ` ( SymGrp ` N ) ) /\ p =/= ( _I |` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = .0. )
30 23 25 28 29 syl3anc 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = .0. )
31 iffalse 
 |-  ( -. p = ( _I |` N ) -> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) = .0. )
32 31 adantl 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) = .0. )
33 32 eqcomd 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> .0. = if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
34 30 33 eqtrd 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) /\ -. p = ( _I |` N ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
35 22 34 pm2.61dan 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ p e. ( Base ` ( SymGrp ` N ) ) ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) = if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
36 35 mpteq2dva 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) ) )
37 36 oveq2d 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` p ) ( .r ` R ) ( G gsum ( k e. N |-> ( ( p ` k ) M k ) ) ) ) ) ) = ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) ) ) )
38 crngring 
 |-  ( R e. CRing -> R e. Ring )
39 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
40 38 39 syl 
 |-  ( R e. CRing -> R e. Mnd )
41 40 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> R e. Mnd )
42 41 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> R e. Mnd )
43 fvexd 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( Base ` ( SymGrp ` N ) ) e. _V )
44 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
45 44 symgid 
 |-  ( N e. Fin -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
46 45 3ad2ant2 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( _I |` N ) = ( 0g ` ( SymGrp ` N ) ) )
47 44 symggrp 
 |-  ( N e. Fin -> ( SymGrp ` N ) e. Grp )
48 47 3ad2ant2 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( SymGrp ` N ) e. Grp )
49 eqid 
 |-  ( 0g ` ( SymGrp ` N ) ) = ( 0g ` ( SymGrp ` N ) )
50 7 49 grpidcl 
 |-  ( ( SymGrp ` N ) e. Grp -> ( 0g ` ( SymGrp ` N ) ) e. ( Base ` ( SymGrp ` N ) ) )
51 48 50 syl 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( 0g ` ( SymGrp ` N ) ) e. ( Base ` ( SymGrp ` N ) ) )
52 46 51 eqeltrd 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( _I |` N ) e. ( Base ` ( SymGrp ` N ) ) )
53 52 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( _I |` N ) e. ( Base ` ( SymGrp ` N ) ) )
54 eqid 
 |-  ( p e. ( Base ` ( SymGrp ` N ) ) |-> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) ) = ( p e. ( Base ` ( SymGrp ` N ) ) |-> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) )
55 eqid 
 |-  ( Base ` R ) = ( Base ` R )
56 4 55 mgpbas 
 |-  ( Base ` R ) = ( Base ` G )
57 4 crngmgp 
 |-  ( R e. CRing -> G e. CMnd )
58 57 3ad2ant1 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> G e. CMnd )
59 58 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> G e. CMnd )
60 simpl2 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> N e. Fin )
61 simpr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ k e. N ) -> k e. N )
62 3 eleq2i 
 |-  ( M e. B <-> M e. ( Base ` A ) )
63 62 biimpi 
 |-  ( M e. B -> M e. ( Base ` A ) )
64 63 3ad2ant3 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> M e. ( Base ` A ) )
65 64 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ k e. N ) -> M e. ( Base ` A ) )
66 2 55 matecl 
 |-  ( ( k e. N /\ k e. N /\ M e. ( Base ` A ) ) -> ( k M k ) e. ( Base ` R ) )
67 61 61 65 66 syl3anc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) /\ k e. N ) -> ( k M k ) e. ( Base ` R ) )
68 67 ralrimiva 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> A. k e. N ( k M k ) e. ( Base ` R ) )
69 56 59 60 68 gsummptcl 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( G gsum ( k e. N |-> ( k M k ) ) ) e. ( Base ` R ) )
70 5 42 43 53 54 69 gsummptif1n0 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( R gsum ( p e. ( Base ` ( SymGrp ` N ) ) |-> if ( p = ( _I |` N ) , ( G gsum ( k e. N |-> ( k M k ) ) ) , .0. ) ) ) = ( G gsum ( k e. N |-> ( k M k ) ) ) )
71 12 37 70 3eqtrd 
 |-  ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> ( D ` M ) = ( G gsum ( k e. N |-> ( k M k ) ) ) )
72 71 ex 
 |-  ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> ( D ` M ) = ( G gsum ( k e. N |-> ( k M k ) ) ) ) )