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	⊢ 𝑆 = ( RSpan ‘ ℤring )
	znzrh2.r	⊢ ∼ = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
	znzrh2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	znzrh2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion	znzrhval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		znzrh2.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
2		znzrh2.r	⊢ ∼ = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
3		znzrh2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4		znzrh2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
5	1 2 3 4	znzrh2	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) )
6	5	fveq1d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐿 ‘ 𝐴 ) = ( ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) ‘ 𝐴 ) )
7		eceq1	⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )
8		eqid	⊢ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ )
9	2	ovexi	⊢ ∼ ∈ V
10		ecexg	⊢ ( ∼ ∈ V → [ 𝐴 ] ∼ ∈ V )
11	9 10	ax-mp	⊢ [ 𝐴 ] ∼ ∈ V
12	7 8 11	fvmpt	⊢ ( 𝐴 ∈ ℤ → ( ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) ‘ 𝐴 ) = [ 𝐴 ] ∼ )
13	6 12	sylan9eq	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ∼ )