Metamath Proof Explorer

Theorem mdet1

Description: The determinant of the identity matrix is 1, i.e. the determinant function is normalized, see also definition in Lang p. 513. (Contributed by SO, 10-Jul-2018) (Proof shortened by AV, 25-Nov-2019)

Ref Expression
Hypotheses mdet1.d 
|- D = ( N maDet R )
mdet1.a 
|- A = ( N Mat R )
mdet1.n 
|- I = ( 1r ` A )
mdet1.o 
|- .1. = ( 1r ` R )
Assertion mdet1 
|- ( ( R e. CRing /\ N e. Fin ) -> ( D ` I ) = .1. )

Proof

Step Hyp Ref Expression
1 mdet1.d 
 |-  D = ( N maDet R )
2 mdet1.a 
 |-  A = ( N Mat R )
3 mdet1.n 
 |-  I = ( 1r ` A )
4 mdet1.o 
 |-  .1. = ( 1r ` R )
5 id 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( R e. CRing /\ N e. Fin ) )
6 crngring 
 |-  ( R e. CRing -> R e. Ring )
7 6 anim1ci 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( N e. Fin /\ R e. Ring ) )
8 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
9 eqid 
 |-  ( Base ` A ) = ( Base ` A )
10 9 3 ringidcl 
 |-  ( A e. Ring -> I e. ( Base ` A ) )
11 7 8 10 3syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> I e. ( Base ` A ) )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 12 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
14 6 13 syl 
 |-  ( R e. CRing -> .1. e. ( Base ` R ) )
15 14 adantr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> .1. e. ( Base ` R ) )
16 5 11 15 jca32 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( R e. CRing /\ N e. Fin ) /\ ( I e. ( Base ` A ) /\ .1. e. ( Base ` R ) ) ) )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 simplr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
19 6 adantr 
 |-  ( ( R e. CRing /\ N e. Fin ) -> R e. Ring )
20 19 adantr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
21 simprl 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
22 simprr 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
23 2 4 17 18 20 21 22 3 mat1ov 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( i e. N /\ j e. N ) ) -> ( i I j ) = if ( i = j , .1. , ( 0g ` R ) ) )
24 23 ralrimivva 
 |-  ( ( R e. CRing /\ N e. Fin ) -> A. i e. N A. j e. N ( i I j ) = if ( i = j , .1. , ( 0g ` R ) ) )
25 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
26 eqid 
 |-  ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
27 1 2 9 25 17 12 26 mdetdiagid 
 |-  ( ( ( R e. CRing /\ N e. Fin ) /\ ( I e. ( Base ` A ) /\ .1. e. ( Base ` R ) ) ) -> ( A. i e. N A. j e. N ( i I j ) = if ( i = j , .1. , ( 0g ` R ) ) -> ( D ` I ) = ( ( # ` N ) ( .g ` ( mulGrp ` R ) ) .1. ) ) )
28 16 24 27 sylc 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( D ` I ) = ( ( # ` N ) ( .g ` ( mulGrp ` R ) ) .1. ) )
29 ringsrg 
 |-  ( R e. Ring -> R e. SRing )
30 6 29 syl 
 |-  ( R e. CRing -> R e. SRing )
31 hashcl 
 |-  ( N e. Fin -> ( # ` N ) e. NN0 )
32 25 26 4 srg1expzeq1 
 |-  ( ( R e. SRing /\ ( # ` N ) e. NN0 ) -> ( ( # ` N ) ( .g ` ( mulGrp ` R ) ) .1. ) = .1. )
33 30 31 32 syl2an 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( ( # ` N ) ( .g ` ( mulGrp ` R ) ) .1. ) = .1. )
34 28 33 eqtrd 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( D ` I ) = .1. )