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=\mathbb{Z}/0\mathbb{Z}$$
	zzngim.2	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
Assertion	zzngim	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpIso}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		zzngim.y	$$⊢Y=\mathbb{Z}/0\mathbb{Z}$$
2		zzngim.2	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	1	zncrng	$$⊢0\in {\mathbb{N}}_0\to Y\in \mathrm{CRing}$$
5		crngring	$$⊢Y\in \mathrm{CRing}\to Y\in \mathrm{Ring}$$
6	3 4 5	mp2b	$$⊢Y\in \mathrm{Ring}$$
7	2	zrhrhm	$$⊢Y\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)$$
8		rhmghm	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}Y\right)$$
9	6 7 8	mp2b	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}Y\right)$$
10		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
11	1 10 2	znzrhfo	$$⊢0\in {\mathbb{N}}_0\to L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Y$$
12	3 11	ax-mp	$$⊢L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Y$$
13		fofn	$$⊢L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Y\to LFn\mathbb{Z}$$
14		fnresdm	$$⊢LFn\mathbb{Z}\to {L\upharpoonright }_{\mathbb{Z}}=L$$
15	12 13 14	mp2b	$$⊢{L\upharpoonright }_{\mathbb{Z}}=L$$
16	2	reseq1i	$$⊢{L\upharpoonright }_{\mathbb{Z}}={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{\mathbb{Z}}$$
17	15 16	eqtr3i	$$⊢L={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{\mathbb{Z}}$$
18		eqid	$$⊢0=0$$
19	18	iftruei	$$⊢if\left(0=0,\mathbb{Z},\left(0..^0\right)\right)=\mathbb{Z}$$
20	19	eqcomi	$$⊢\mathbb{Z}=if\left(0=0,\mathbb{Z},\left(0..^0\right)\right)$$
21	1 10 17 20	znf1o	$$⊢0\in {\mathbb{N}}_0\to L:\mathbb{Z}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Y$$
22	3 21	ax-mp	$$⊢L:\mathbb{Z}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Y$$
23		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
24	23 10	isgim	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpIso}Y\right)\leftrightarrow \left(L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}Y\right)\wedge L:\mathbb{Z}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Y\right)$$
25	9 22 24	mpbir2an	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpIso}Y\right)$$