This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = RSpan (ℤ_{ring})$
		znzrh2.r	$⊢ \underset{˙}{\sim} = ℤ_{ring} ~_{QG} S (\{N\})$
		znzrh2.y	$⊢ Y = ℤ / N ℤ$
		znzrh2.2	$⊢ L = ℤRHom (Y)$
	Assertion	znzrhval	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L (A) = [A] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		znzrh2.s	$⊢ S = RSpan (ℤ_{ring})$
2		znzrh2.r	$⊢ \underset{˙}{\sim} = ℤ_{ring} ~_{QG} S (\{N\})$
3		znzrh2.y	$⊢ Y = ℤ / N ℤ$
4		znzrh2.2	$⊢ L = ℤRHom (Y)$
5	1 2 3 4	znzrh2	$⊢ N \in ℕ_{0} \to L = (x \in ℤ ⟼ [x] \underset{˙}{\sim})$
6	5	fveq1d	$⊢ N \in ℕ_{0} \to L (A) = (x \in ℤ ⟼ [x] \underset{˙}{\sim}) (A)$
7		eceq1	$⊢ x = A \to [x] \underset{˙}{\sim} = [A] \underset{˙}{\sim}$
8		eqid	$⊢ (x \in ℤ ⟼ [x] \underset{˙}{\sim}) = (x \in ℤ ⟼ [x] \underset{˙}{\sim})$
9	2	ovexi	$⊢ \underset{˙}{\sim} \in V$
10		ecexg	$⊢ \underset{˙}{\sim} \in V \to [A] \underset{˙}{\sim} \in V$
11	9 10	ax-mp	$⊢ [A] \underset{˙}{\sim} \in V$
12	7 8 11	fvmpt	$⊢ A \in ℤ \to (x \in ℤ ⟼ [x] \underset{˙}{\sim}) (A) = [A] \underset{˙}{\sim}$
13	6 12	sylan9eq	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L (A) = [A] \underset{˙}{\sim}$