Metamath Proof Explorer

Theorem mdetdiagid

Description: The determinant of a diagonal matrix with identical entries is the power of the entry 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 )
mdetdiagid.c 
|- C = ( Base ` R )
mdetdiagid.t 
|- .x. = ( .g ` G )
Assertion mdetdiagid 
|- ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> ( D ` M ) = ( ( # ` N ) .x. X ) ) )

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 mdetdiagid.c 
 |-  C = ( Base ` R )
7 mdetdiagid.t 
 |-  .x. = ( .g ` G )
8 simpl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> R e. CRing )
9 8 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> R e. CRing )
10 simpr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> N e. Fin )
11 10 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> N e. Fin )
12 simpl 
 |-  ( ( M e. B /\ X e. C ) -> M e. B )
13 12 adantl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> M e. B )
14 9 11 13 3jca 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> ( R e. CRing /\ N e. Fin /\ M e. B ) )
15 14 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( R e. CRing /\ N e. Fin /\ M e. B ) )
16 id 
 |-  ( ( i M j ) = if ( i = j , X , .0. ) -> ( i M j ) = if ( i = j , X , .0. ) )
17 ifnefalse 
 |-  ( i =/= j -> if ( i = j , X , .0. ) = .0. )
18 17 adantl 
 |-  ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) -> if ( i = j , X , .0. ) = .0. )
19 16 18 sylan9eqr 
 |-  ( ( ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ i e. N ) /\ j e. N ) /\ i =/= j ) /\ ( i M j ) = if ( i = j , X , .0. ) ) -> ( i M j ) = .0. )
20 19 exp31 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ i e. N ) /\ j e. N ) -> ( i =/= j -> ( ( i M j ) = if ( i = j , X , .0. ) -> ( i M j ) = .0. ) ) )
21 20 com23 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ i e. N ) /\ j e. N ) -> ( ( i M j ) = if ( i = j , X , .0. ) -> ( i =/= j -> ( i M j ) = .0. ) ) )
22 21 ralimdva 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ i e. N ) -> ( A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) )
23 22 ralimdva 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) )
24 23 imp 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) )
25 1 2 3 4 5 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 ) ) ) ) )
26 15 24 25 sylc 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( D ` M ) = ( G gsum ( k e. N |-> ( k M k ) ) ) )
27 oveq1 
 |-  ( i = k -> ( i M j ) = ( k M j ) )
28 equequ1 
 |-  ( i = k -> ( i = j <-> k = j ) )
29 28 ifbid 
 |-  ( i = k -> if ( i = j , X , .0. ) = if ( k = j , X , .0. ) )
30 27 29 eqeq12d 
 |-  ( i = k -> ( ( i M j ) = if ( i = j , X , .0. ) <-> ( k M j ) = if ( k = j , X , .0. ) ) )
31 oveq2 
 |-  ( j = k -> ( k M j ) = ( k M k ) )
32 equequ2 
 |-  ( j = k -> ( k = j <-> k = k ) )
33 32 ifbid 
 |-  ( j = k -> if ( k = j , X , .0. ) = if ( k = k , X , .0. ) )
34 31 33 eqeq12d 
 |-  ( j = k -> ( ( k M j ) = if ( k = j , X , .0. ) <-> ( k M k ) = if ( k = k , X , .0. ) ) )
35 30 34 rspc2v 
 |-  ( ( k e. N /\ k e. N ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> ( k M k ) = if ( k = k , X , .0. ) ) )
36 35 anidms 
 |-  ( k e. N -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> ( k M k ) = if ( k = k , X , .0. ) ) )
37 36 adantl 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ k e. N ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> ( k M k ) = if ( k = k , X , .0. ) ) )
38 37 imp 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ k e. N ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( k M k ) = if ( k = k , X , .0. ) )
39 equid 
 |-  k = k
40 39 iftruei 
 |-  if ( k = k , X , .0. ) = X
41 38 40 eqtrdi 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ k e. N ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( k M k ) = X )
42 41 an32s 
 |-  ( ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) /\ k e. N ) -> ( k M k ) = X )
43 42 mpteq2dva 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( k e. N |-> ( k M k ) ) = ( k e. N |-> X ) )
44 43 oveq2d 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( G gsum ( k e. N |-> ( k M k ) ) ) = ( G gsum ( k e. N |-> X ) ) )
45 4 crngmgp 
 |-  ( R e. CRing -> G e. CMnd )
46 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
47 45 46 syl 
 |-  ( R e. CRing -> G e. Mnd )
48 47 adantr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> G e. Mnd )
49 simpr 
 |-  ( ( M e. B /\ X e. C ) -> X e. C )
50 4 6 mgpbas 
 |-  C = ( Base ` G )
51 50 7 gsumconst 
 |-  ( ( G e. Mnd /\ N e. Fin /\ X e. C ) -> ( G gsum ( k e. N |-> X ) ) = ( ( # ` N ) .x. X ) )
52 48 10 49 51 syl2an3an 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> ( G gsum ( k e. N |-> X ) ) = ( ( # ` N ) .x. X ) )
53 52 adantr 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( G gsum ( k e. N |-> X ) ) = ( ( # ` N ) .x. X ) )
54 26 44 53 3eqtrd 
 |-  ( ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) /\ A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) ) -> ( D ` M ) = ( ( # ` N ) .x. X ) )
55 54 ex 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> ( D ` M ) = ( ( # ` N ) .x. X ) ) )