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	⊢ 𝑌 = ( ℤ/nℤ ‘ 0 )
	zzngim.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion	zzngim	⊢ 𝐿 ∈ ( ℤ_ring GrpIso 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		zzngim.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 0 )
2		zzngim.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
3		0nn0	⊢ 0 ∈ ℕ₀
4	1	zncrng	⊢ ( 0 ∈ ℕ₀ → 𝑌 ∈ CRing )
5		crngring	⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
6	3 4 5	mp2b	⊢ 𝑌 ∈ Ring
7	2	zrhrhm	⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤ_ring RingHom 𝑌 ) )
8		rhmghm	⊢ ( 𝐿 ∈ ( ℤ_ring RingHom 𝑌 ) → 𝐿 ∈ ( ℤ_ring GrpHom 𝑌 ) )
9	6 7 8	mp2b	⊢ 𝐿 ∈ ( ℤ_ring GrpHom 𝑌 )
10		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11	1 10 2	znzrhfo	⊢ ( 0 ∈ ℕ₀ → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
12	3 11	ax-mp	⊢ 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 )
13		fofn	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) → 𝐿 Fn ℤ )
14		fnresdm	⊢ ( 𝐿 Fn ℤ → ( 𝐿 ↾ ℤ ) = 𝐿 )
15	12 13 14	mp2b	⊢ ( 𝐿 ↾ ℤ ) = 𝐿
16	2	reseq1i	⊢ ( 𝐿 ↾ ℤ ) = ( ( ℤRHom ‘ 𝑌 ) ↾ ℤ )
17	15 16	eqtr3i	⊢ 𝐿 = ( ( ℤRHom ‘ 𝑌 ) ↾ ℤ )
18		eqid	⊢ 0 = 0
19	18	iftruei	⊢ if ( 0 = 0 , ℤ , ( 0 ..^ 0 ) ) = ℤ
20	19	eqcomi	⊢ ℤ = if ( 0 = 0 , ℤ , ( 0 ..^ 0 ) )
21	1 10 17 20	znf1o	⊢ ( 0 ∈ ℕ₀ → 𝐿 : ℤ –1-1-onto→ ( Base ‘ 𝑌 ) )
22	3 21	ax-mp	⊢ 𝐿 : ℤ –1-1-onto→ ( Base ‘ 𝑌 )
23		zringbas	⊢ ℤ = ( Base ‘ ℤ_ring )
24	23 10	isgim	⊢ ( 𝐿 ∈ ( ℤ_ring GrpIso 𝑌 ) ↔ ( 𝐿 ∈ ( ℤ_ring GrpHom 𝑌 ) ∧ 𝐿 : ℤ –1-1-onto→ ( Base ‘ 𝑌 ) ) )
25	9 22 24	mpbir2an	⊢ 𝐿 ∈ ( ℤ_ring GrpIso 𝑌 )

Metamath Proof Explorer

Theorem zzngim

Proof