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 )