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 ‘ 𝑌 ) )