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=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znval2.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
	znval2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
Assertion	znzrh	$$⊢N\in {\mathbb{N}}_0\to \mathrm{\mathbb{Z}RHom}\left(U\right)=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		znval2.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znval2.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
3		znval2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
4		eqidd	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_U={\mathrm{Base}}_U$$
5	1 2 3	znbas2	$$⊢N\in {\mathbb{N}}_0\to {\mathrm{Base}}_U={\mathrm{Base}}_Y$$
6	1 2 3	znadd	$$⊢N\in {\mathbb{N}}_0\to {+}_U={+}_Y$$
7	6	oveqdr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in {\mathrm{Base}}_U\wedge y\in {\mathrm{Base}}_U\right)\right)\to x{+}_{U}y=x{+}_{Y}y$$
8	1 2 3	znmul	$$⊢N\in {\mathbb{N}}_0\to {\cdot }_U={\cdot }_Y$$
9	8	oveqdr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(x\in {\mathrm{Base}}_U\wedge y\in {\mathrm{Base}}_U\right)\right)\to x{\cdot }_{U}y=x{\cdot }_{Y}y$$
10	4 5 7 9	zrhpropd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{\mathbb{Z}RHom}\left(U\right)=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$