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=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znzrh2.r	$$⊢\underset{\dot{}}{\sim }={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)$$
	znzrh2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znzrh2.2	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
Assertion	znzrh2	$$⊢N\in {\mathbb{N}}_0\to L=\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$

Proof

Step	Hyp	Ref	Expression
1		znzrh2.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znzrh2.r	$$⊢\underset{\dot{}}{\sim }={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)$$
3		znzrh2.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
4		znzrh2.2	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
5		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
6		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
7	1	znlidl	$$⊢N\in \mathbb{Z}\to S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
8	6 7	syl	$$⊢N\in {\mathbb{N}}_0\to S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
9	2	oveq2i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
10		zringcrng	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
11		eqid	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
12	11	crng2idl	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}\to \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
13	10 12	ax-mp	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{2Ideal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
14		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
15		eceq2	$$⊢\underset{\dot{}}{\sim }={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\to \left[x\right]\underset{\dot{}}{\sim }=\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
16	2 15	ax-mp	$$⊢\left[x\right]\underset{\dot{}}{\sim }=\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
17	16	mpteq2i	$$⊢\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)\right)$$
18	9 13 14 17	qusrhm	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\to \left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)\right)$$
19	5 8 18	sylancr	$$⊢N\in {\mathbb{N}}_0\to \left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)\right)$$
20	1 9	zncrng2	$$⊢N\in \mathbb{Z}\to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\in \mathrm{CRing}$$
21		crngring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\in \mathrm{CRing}\to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\in \mathrm{Ring}$$
22		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)=\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)$$
23	22	zrhrhmb	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\in \mathrm{Ring}\to \left(\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)\right)\leftrightarrow \left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)\right)$$
24	6 20 21 23	4syl	$$⊢N\in {\mathbb{N}}_0\to \left(\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)\right)\leftrightarrow \left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)\right)$$
25	19 24	mpbid	$$⊢N\in {\mathbb{N}}_0\to \left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)$$
26	1 9 3	znzrh	$$⊢N\in {\mathbb{N}}_0\to \mathrm{\mathbb{Z}RHom}\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\underset{\dot{}}{\sim }\right)=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
27	25 26	eqtr2d	$$⊢N\in {\mathbb{N}}_0\to \mathrm{\mathbb{Z}RHom}\left(Y\right)=\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
28	4 27	syl5eq	$$⊢N\in {\mathbb{N}}_0\to L=\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$