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 )