This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znzrhval

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 znzrhval 
|- ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ )

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 1 2 3 4 znzrh2 
 |-  ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) )
6 5 fveq1d 
 |-  ( N e. NN0 -> ( L ` A ) = ( ( x e. ZZ |-> [ x ] .~ ) ` A ) )
7 eceq1 
 |-  ( x = A -> [ x ] .~ = [ A ] .~ )
8 eqid 
 |-  ( x e. ZZ |-> [ x ] .~ ) = ( x e. ZZ |-> [ x ] .~ )
9 2 ovexi 
 |-  .~ e. _V
10 ecexg 
 |-  ( .~ e. _V -> [ A ] .~ e. _V )
11 9 10 ax-mp 
 |-  [ A ] .~ e. _V
12 7 8 11 fvmpt 
 |-  ( A e. ZZ -> ( ( x e. ZZ |-> [ x ] .~ ) ` A ) = [ A ] .~ )
13 6 12 sylan9eq 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ )