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 ⊢ 𝑆 = ( 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 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ∼ )