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 ] .~ )