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 𝐷 = ( 𝑁 maDet 𝑅 )
mdet1.a 𝐴 = ( 𝑁 Mat 𝑅 )
mdet1.n 𝐼 = ( 1r𝐴 )
mdet1.o 1 = ( 1r𝑅 )
Assertion mdet1 ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝐷𝐼 ) = 1 )

Proof

Step Hyp Ref Expression
1 mdet1.d 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdet1.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mdet1.n 𝐼 = ( 1r𝐴 )
4 mdet1.o 1 = ( 1r𝑅 )
5 id ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) )
6 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
7 6 anim1ci ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
8 2 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
9 eqid ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
10 9 3 ringidcl ( 𝐴 ∈ Ring → 𝐼 ∈ ( Base ‘ 𝐴 ) )
11 7 8 10 3syl ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐼 ∈ ( Base ‘ 𝐴 ) )
12 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 12 4 ringidcl ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
14 6 13 syl ( 𝑅 ∈ CRing → 1 ∈ ( Base ‘ 𝑅 ) )
15 14 adantr ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 1 ∈ ( Base ‘ 𝑅 ) )
16 5 11 15 jca32 ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ ( Base ‘ 𝐴 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) ) )
17 eqid ( 0g𝑅 ) = ( 0g𝑅 )
18 simplr ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑁 ∈ Fin )
19 6 adantr ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝑅 ∈ Ring )
20 19 adantr ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
21 simprl ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖𝑁 )
22 simprr ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑗𝑁 )
23 2 4 17 18 20 21 22 3 mat1ov ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 𝐼 𝑗 ) = if ( 𝑖 = 𝑗 , 1 , ( 0g𝑅 ) ) )
24 23 ralrimivva ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐼 𝑗 ) = if ( 𝑖 = 𝑗 , 1 , ( 0g𝑅 ) ) )
25 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
26 eqid ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
27 1 2 9 25 17 12 26 mdetdiagid ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝐼 ∈ ( Base ‘ 𝐴 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐼 𝑗 ) = if ( 𝑖 = 𝑗 , 1 , ( 0g𝑅 ) ) → ( 𝐷𝐼 ) = ( ( ♯ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 1 ) ) )
28 16 24 27 sylc ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝐷𝐼 ) = ( ( ♯ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 1 ) )
29 ringsrg ( 𝑅 ∈ Ring → 𝑅 ∈ SRing )
30 6 29 syl ( 𝑅 ∈ CRing → 𝑅 ∈ SRing )
31 hashcl ( 𝑁 ∈ Fin → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
32 25 26 4 srg1expzeq1 ( ( 𝑅 ∈ SRing ∧ ( ♯ ‘ 𝑁 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 1 ) = 1 )
33 30 31 32 syl2an ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ♯ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 1 ) = 1 )
34 28 33 eqtrd ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝐷𝐼 ) = 1 )