# Metamath Proof Explorer

## Theorem znzrh2

Description: The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znzrh2.s ${⊢}{S}=\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)$
znzrh2.r
znzrh2.y ${⊢}{Y}=ℤ/{N}ℤ$
znzrh2.2 ${⊢}{L}=\mathrm{ℤRHom}\left({Y}\right)$
Assertion znzrh2

### Proof

Step Hyp Ref Expression
1 znzrh2.s ${⊢}{S}=\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)$
2 znzrh2.r
3 znzrh2.y ${⊢}{Y}=ℤ/{N}ℤ$
4 znzrh2.2 ${⊢}{L}=\mathrm{ℤRHom}\left({Y}\right)$
5 zringring ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
6 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
7 1 znlidl ${⊢}{N}\in ℤ\to {S}\left(\left\{{N}\right\}\right)\in \mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)$
8 6 7 syl ${⊢}{N}\in {ℕ}_{0}\to {S}\left(\left\{{N}\right\}\right)\in \mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)$
9 2 oveq2i
10 zringcrng ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{CRing}$
11 eqid ${⊢}\mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)=\mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)$
12 11 crng2idl ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{CRing}\to \mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)=\mathrm{2Ideal}\left({ℤ}_{\mathrm{ring}}\right)$
13 10 12 ax-mp ${⊢}\mathrm{LIdeal}\left({ℤ}_{\mathrm{ring}}\right)=\mathrm{2Ideal}\left({ℤ}_{\mathrm{ring}}\right)$
14 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
15 eceq2
16 2 15 ax-mp
17 16 mpteq2i
18 9 13 14 17 qusrhm
19 5 8 18 sylancr
20 1 9 zncrng2
21 crngring
22 eqid
23 22 zrhrhmb
24 6 20 21 23 4syl
25 19 24 mpbid
26 1 9 3 znzrh
27 25 26 eqtr2d
28 4 27 syl5eq