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 ⊢ S = RSpan ⁡ ℤ ring
znval2.u ⊢ U = ℤ ring / 𝑠 ℤ ring ~ QG S ⁡ N
znval2.y ⊢ Y = ℤ/Nℤ
Assertion znzrh ⊢ N ∈ ℕ 0 → ℤRHom ⁡ U = ℤRHom ⁡ Y

Proof

Step Hyp Ref Expression
1 znval2.s ⊢ S = RSpan ⁡ ℤ ring
2 znval2.u ⊢ U = ℤ ring / 𝑠 ℤ ring ~ QG S ⁡ N
3 znval2.y ⊢ Y = ℤ/Nℤ
4 eqidd ⊢ N ∈ ℕ 0 → Base U = Base U
5 1 2 3 znbas2 ⊢ N ∈ ℕ 0 → Base U = Base Y
6 1 2 3 znadd ⊢ N ∈ ℕ 0 → + U = + Y
7 6 oveqdr ⊢ N ∈ ℕ 0 ∧ x ∈ Base U ∧ y ∈ Base U → x + U y = x + Y y
8 1 2 3 znmul ⊢ N ∈ ℕ 0 → ⋅ U = ⋅ Y
9 8 oveqdr ⊢ N ∈ ℕ 0 ∧ x ∈ Base U ∧ y ∈ Base U → x ⋅ U y = x ⋅ Y y
10 4 5 7 9 zrhpropd ⊢ N ∈ ℕ 0 → ℤRHom ⁡ U = ℤRHom ⁡ Y