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=\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	znzrhval	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in \mathbb{Z}\right)\to L\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$

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	1 2 3 4	znzrh2	$$⊢N\in {\mathbb{N}}_0\to L=\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
6	5	fveq1d	$$⊢N\in {\mathbb{N}}_0\to L\left(A\right)=\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)\left(A\right)$$
7		eceq1	$$⊢x=A\to \left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$
8		eqid	$$⊢\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
9	2	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
10		ecexg	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}\to \left[A\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
11	9 10	ax-mp	$$⊢\left[A\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
12	7 8 11	fvmpt	$$⊢A\in \mathbb{Z}\to \left(x\in \mathbb{Z}⟼\left[x\right]\underset{\dot{}}{\sim }\right)\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$
13	6 12	sylan9eq	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in \mathbb{Z}\right)\to L\left(A\right)=\left[A\right]\underset{\dot{}}{\sim }$$