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 = ( RSpan ` ZZring )
znzrh2.r 
|- .~ = ( ZZring ~QG ( S ` { N } ) )
znzrh2.y 
|- Y = ( Z/nZ ` N )
znzrh2.2 
|- L = ( ZRHom ` Y )
Assertion znzrh2 
|- ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) )

Proof

Step Hyp Ref Expression
1 znzrh2.s 
 |-  S = ( RSpan ` ZZring )
2 znzrh2.r 
 |-  .~ = ( ZZring ~QG ( S ` { N } ) )
3 znzrh2.y 
 |-  Y = ( Z/nZ ` N )
4 znzrh2.2 
 |-  L = ( ZRHom ` Y )
5 zringring 
 |-  ZZring e. Ring
6 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
7 1 znlidl 
 |-  ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )
8 6 7 syl 
 |-  ( N e. NN0 -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )
9 2 oveq2i 
 |-  ( ZZring /s .~ ) = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
10 zringcrng 
 |-  ZZring e. CRing
11 eqid 
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
12 11 crng2idl 
 |-  ( ZZring e. CRing -> ( LIdeal ` ZZring ) = ( 2Ideal ` ZZring ) )
13 10 12 ax-mp 
 |-  ( LIdeal ` ZZring ) = ( 2Ideal ` ZZring )
14 zringbas 
 |-  ZZ = ( Base ` ZZring )
15 eceq2 
 |-  ( .~ = ( ZZring ~QG ( S ` { N } ) ) -> [ x ] .~ = [ x ] ( ZZring ~QG ( S ` { N } ) ) )
16 2 15 ax-mp 
 |-  [ x ] .~ = [ x ] ( ZZring ~QG ( S ` { N } ) )
17 16 mpteq2i 
 |-  ( x e. ZZ |-> [ x ] .~ ) = ( x e. ZZ |-> [ x ] ( ZZring ~QG ( S ` { N } ) ) )
18 9 13 14 17 qusrhm 
 |-  ( ( ZZring e. Ring /\ ( S ` { N } ) e. ( LIdeal ` ZZring ) ) -> ( x e. ZZ |-> [ x ] .~ ) e. ( ZZring RingHom ( ZZring /s .~ ) ) )
19 5 8 18 sylancr 
 |-  ( N e. NN0 -> ( x e. ZZ |-> [ x ] .~ ) e. ( ZZring RingHom ( ZZring /s .~ ) ) )
20 1 9 zncrng2 
 |-  ( N e. ZZ -> ( ZZring /s .~ ) e. CRing )
21 crngring 
 |-  ( ( ZZring /s .~ ) e. CRing -> ( ZZring /s .~ ) e. Ring )
22 eqid 
 |-  ( ZRHom ` ( ZZring /s .~ ) ) = ( ZRHom ` ( ZZring /s .~ ) )
23 22 zrhrhmb 
 |-  ( ( ZZring /s .~ ) e. Ring -> ( ( x e. ZZ |-> [ x ] .~ ) e. ( ZZring RingHom ( ZZring /s .~ ) ) <-> ( x e. ZZ |-> [ x ] .~ ) = ( ZRHom ` ( ZZring /s .~ ) ) ) )
24 6 20 21 23 4syl 
 |-  ( N e. NN0 -> ( ( x e. ZZ |-> [ x ] .~ ) e. ( ZZring RingHom ( ZZring /s .~ ) ) <-> ( x e. ZZ |-> [ x ] .~ ) = ( ZRHom ` ( ZZring /s .~ ) ) ) )
25 19 24 mpbid 
 |-  ( N e. NN0 -> ( x e. ZZ |-> [ x ] .~ ) = ( ZRHom ` ( ZZring /s .~ ) ) )
26 1 9 3 znzrh 
 |-  ( N e. NN0 -> ( ZRHom ` ( ZZring /s .~ ) ) = ( ZRHom ` Y ) )
27 25 26 eqtr2d 
 |-  ( N e. NN0 -> ( ZRHom ` Y ) = ( x e. ZZ |-> [ x ] .~ ) )
28 4 27 eqtrid 
 |-  ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) )