Theorem znzrhfo

Description: The ZZ ring homomorphism is a surjection onto ZZ / n ZZ . (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	znzrhfo.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znzrhfo.b	$$⊢B={\mathrm{Base}}_Y$$
	znzrhfo.2	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
Assertion	znzrhfo	$$⊢N\in {\mathbb{N}}_0\to L:\mathbb{Z}\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		znzrhfo.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		znzrhfo.b	$$⊢B={\mathrm{Base}}_Y$$
3		znzrhfo.2	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
4		eqidd	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)$$
5		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
6	5	a1i	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
7		eqid	$$⊢\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)=\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)$$
8		ovexd	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\in \mathrm{V}$$
9		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
10	9	a1i	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
11	4 6 7 8 10	quslem	$$⊢N\in {\mathbb{N}}_0\to \left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}\mathbb{Z}/\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)$$
12		eqid	$$⊢\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
13		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)$$
14	12 1 13	znbas	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)={\mathrm{Base}}_Y$$
15	14 2	eqtr4di	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)=B$$
16		foeq3	$$⊢\mathbb{Z}/\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)=B\to \left(\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}\mathbb{Z}/\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\leftrightarrow \left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}B\right)$$
17	15 16	syl	$$⊢N\in {\mathbb{N}}_0\to \left(\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}\mathbb{Z}/\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\leftrightarrow \left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}B\right)$$
18	11 17	mpbid	$$⊢N\in {\mathbb{N}}_0\to \left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}B$$
19	12 13 1 3	znzrh2	$$⊢N\in {\mathbb{N}}_0\to L=\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)$$
20		foeq1	$$⊢L=\left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right)\to \left(L:\mathbb{Z}\underset{onto}{⟶}B\leftrightarrow \left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}B\right)$$
21	19 20	syl	$$⊢N\in {\mathbb{N}}_0\to \left(L:\mathbb{Z}\underset{onto}{⟶}B\leftrightarrow \left(x\in \mathbb{Z}⟼\left[x\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{N\right\}\right)\right)\right):\mathbb{Z}\underset{onto}{⟶}B\right)$$
22	18 21	mpbird	$$⊢N\in {\mathbb{N}}_0\to L:\mathbb{Z}\underset{onto}{⟶}B$$