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

Metamath Proof Explorer

Theorem znzrh

Description: The ZZ ring homomorphism of Z/nZ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znval2.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
znval2.u ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
znval2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion znzrh ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑈 ) = ( ℤRHom ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 znval2.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
2 znval2.u ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3 znval2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4 eqidd ⊢ ( 𝑁 ∈ ℕ0 → ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) )
5 1 2 3 znbas2 ⊢ ( 𝑁 ∈ ℕ0 → ( Base ‘ 𝑈 ) = ( Base ‘ 𝑌 ) )
6 1 2 3 znadd ⊢ ( 𝑁 ∈ ℕ0 → ( +g ‘ 𝑈 ) = ( +g ‘ 𝑌 ) )
7 6 oveqdr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑌 ) 𝑦 ) )
8 1 2 3 znmul ⊢ ( 𝑁 ∈ ℕ0 → ( .r ‘ 𝑈 ) = ( .r ‘ 𝑌 ) )
9 8 oveqdr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑥 ( .r ‘ 𝑈 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑌 ) 𝑦 ) )
10 4 5 7 9 zrhpropd ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑈 ) = ( ℤRHom ‘ 𝑌 ) )