This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zzngim

Description: The ZZ ring homomorphism is an isomorphism for N = 0 . (We only show group isomorphism here, but ring isomorphism follows, since it is a bijective ring homomorphism.) (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses zzngim.y 
|- Y = ( Z/nZ ` 0 )
zzngim.2 
|- L = ( ZRHom ` Y )
Assertion zzngim 
|- L e. ( ZZring GrpIso Y )

Proof

Step Hyp Ref Expression
1 zzngim.y 
 |-  Y = ( Z/nZ ` 0 )
2 zzngim.2 
 |-  L = ( ZRHom ` Y )
3 0nn0 
 |-  0 e. NN0
4 1 zncrng 
 |-  ( 0 e. NN0 -> Y e. CRing )
5 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
6 3 4 5 mp2b 
 |-  Y e. Ring
7 2 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
8 rhmghm 
 |-  ( L e. ( ZZring RingHom Y ) -> L e. ( ZZring GrpHom Y ) )
9 6 7 8 mp2b 
 |-  L e. ( ZZring GrpHom Y )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 1 10 2 znzrhfo 
 |-  ( 0 e. NN0 -> L : ZZ -onto-> ( Base ` Y ) )
12 3 11 ax-mp 
 |-  L : ZZ -onto-> ( Base ` Y )
13 fofn 
 |-  ( L : ZZ -onto-> ( Base ` Y ) -> L Fn ZZ )
14 fnresdm 
 |-  ( L Fn ZZ -> ( L |` ZZ ) = L )
15 12 13 14 mp2b 
 |-  ( L |` ZZ ) = L
16 2 reseq1i 
 |-  ( L |` ZZ ) = ( ( ZRHom ` Y ) |` ZZ )
17 15 16 eqtr3i 
 |-  L = ( ( ZRHom ` Y ) |` ZZ )
18 eqid 
 |-  0 = 0
19 18 iftruei 
 |-  if ( 0 = 0 , ZZ , ( 0 ..^ 0 ) ) = ZZ
20 19 eqcomi 
 |-  ZZ = if ( 0 = 0 , ZZ , ( 0 ..^ 0 ) )
21 1 10 17 20 znf1o 
 |-  ( 0 e. NN0 -> L : ZZ -1-1-onto-> ( Base ` Y ) )
22 3 21 ax-mp 
 |-  L : ZZ -1-1-onto-> ( Base ` Y )
23 zringbas 
 |-  ZZ = ( Base ` ZZring )
24 23 10 isgim 
 |-  ( L e. ( ZZring GrpIso Y ) <-> ( L e. ( ZZring GrpHom Y ) /\ L : ZZ -1-1-onto-> ( Base ` Y ) ) )
25 9 22 24 mpbir2an 
 |-  L e. ( ZZring GrpIso Y )