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 = ℤ/ 0 ℤ
zzngim.2 ⊢ L = ℤRHom ⁡ Y
Assertion zzngim ⊢ L ∈ ℤ ring GrpIso Y

Proof

Step Hyp Ref Expression
1 zzngim.y ⊢ Y = ℤ/ 0 ℤ
2 zzngim.2 ⊢ L = ℤRHom ⁡ Y
3 0nn0 ⊢ 0 ∈ ℕ 0
4 1 zncrng ⊢ 0 ∈ ℕ 0 → Y ∈ CRing
5 crngring ⊢ Y ∈ CRing → Y ∈ Ring
6 3 4 5 mp2b ⊢ Y ∈ Ring
7 2 zrhrhm ⊢ Y ∈ Ring → L ∈ ℤ ring RingHom Y
8 rhmghm ⊢ L ∈ ℤ ring RingHom Y → L ∈ ℤ ring GrpHom Y
9 6 7 8 mp2b ⊢ L ∈ ℤ ring GrpHom Y
10 eqid ⊢ Base Y = Base Y
11 1 10 2 znzrhfo ⊢ 0 ∈ ℕ 0 → L : ℤ ⟶ onto Base Y
12 3 11 ax-mp ⊢ L : ℤ ⟶ onto Base Y
13 fofn ⊢ L : ℤ ⟶ onto Base Y → L Fn ℤ
14 fnresdm ⊢ L Fn ℤ → L ↾ ℤ = L
15 12 13 14 mp2b ⊢ L ↾ ℤ = L
16 2 reseq1i ⊢ L ↾ ℤ = ℤRHom ⁡ Y ↾ ℤ
17 15 16 eqtr3i ⊢ L = ℤRHom ⁡ Y ↾ ℤ
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 ∈ ℕ 0 → L : ℤ ⟶ 1-1 onto Base Y
22 3 21 ax-mp ⊢ L : ℤ ⟶ 1-1 onto Base Y
23 zringbas ⊢ ℤ = Base ℤ ring
24 23 10 isgim ⊢ L ∈ ℤ ring GrpIso Y ↔ L ∈ ℤ ring GrpHom Y ∧ L : ℤ ⟶ 1-1 onto Base Y
25 9 22 24 mpbir2an ⊢ L ∈ ℤ ring GrpIso Y