Metamath Proof Explorer

Theorem znzrh2

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 znzrh2 ( 𝑁 ∈ ℕ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 zringring ⊢ ℤring ∈ Ring
6 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
7 1 znlidl ⊢ ( 𝑁 ∈ ℤ → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
9 2 oveq2i ⊢ ( ℤring /s ∼ ) = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
10 zringcrng ⊢ ℤring ∈ CRing
11 eqid ⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
12 11 crng2idl ⊢ ( ℤring ∈ CRing → ( LIdeal ‘ ℤring ) = ( 2Ideal ‘ ℤring ) )
13 10 12 ax-mp ⊢ ( LIdeal ‘ ℤring ) = ( 2Ideal ‘ ℤring )
14 zringbas ⊢ ℤ = ( Base ‘ ℤring )
15 eceq2 ⊢ ( ∼ = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) → [ 𝑥 ] ∼ = [ 𝑥 ] ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
16 2 15 ax-mp ⊢ [ 𝑥 ] ∼ = [ 𝑥 ] ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
17 16 mpteq2i ⊢ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
18 9 13 14 17 qusrhm ⊢ ( ( ℤring ∈ Ring ∧ ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) ) → ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) ∈ ( ℤring RingHom ( ℤring /s ∼ ) ) )
19 5 8 18 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) ∈ ( ℤring RingHom ( ℤring /s ∼ ) ) )
20 1 9 zncrng2 ⊢ ( 𝑁 ∈ ℤ → ( ℤring /s ∼ ) ∈ CRing )
21 crngring ⊢ ( ( ℤring /s ∼ ) ∈ CRing → ( ℤring /s ∼ ) ∈ Ring )
22 eqid ⊢ ( ℤRHom ‘ ( ℤring /s ∼ ) ) = ( ℤRHom ‘ ( ℤring /s ∼ ) )
23 22 zrhrhmb ⊢ ( ( ℤring /s ∼ ) ∈ Ring → ( ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) ∈ ( ℤring RingHom ( ℤring /s ∼ ) ) ↔ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) = ( ℤRHom ‘ ( ℤring /s ∼ ) ) ) )
24 6 20 21 23 4syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) ∈ ( ℤring RingHom ( ℤring /s ∼ ) ) ↔ ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) = ( ℤRHom ‘ ( ℤring /s ∼ ) ) ) )
25 19 24 mpbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) = ( ℤRHom ‘ ( ℤring /s ∼ ) ) )
26 1 9 3 znzrh ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ ( ℤring /s ∼ ) ) = ( ℤRHom ‘ 𝑌 ) )
27 25 26 eqtr2d ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑌 ) = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) )
28 4 27 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 = ( 𝑥 ∈ ℤ ↦ [ 𝑥 ] ∼ ) )