Theorem znzrh

Description: The ZZ ring homomorphism of Z/nZ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znval2.s	|- S = ( RSpan ` ZZring )
	znval2.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
	znval2.y	|- Y = ( Z/nZ ` N )
Assertion	znzrh	|- ( N e. NN0 -> ( ZRHom ` U ) = ( ZRHom ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		znval2.s	|- S = ( RSpan ` ZZring )
2		znval2.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3		znval2.y	|- Y = ( Z/nZ ` N )
4		eqidd	|- ( N e. NN0 -> ( Base ` U ) = ( Base ` U ) )
5	1 2 3	znbas2	|- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) )
6	1 2 3	znadd	|- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) )
7	6	oveqdr	|- ( ( N e. NN0 /\ ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) ) -> ( x ( +g ` U ) y ) = ( x ( +g ` Y ) y ) )
8	1 2 3	znmul	|- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) )
9	8	oveqdr	|- ( ( N e. NN0 /\ ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) ) -> ( x ( .r ` U ) y ) = ( x ( .r ` Y ) y ) )
10	4 5 7 9	zrhpropd	|- ( N e. NN0 -> ( ZRHom ` U ) = ( ZRHom ` Y ) )