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

Metamath Proof Explorer

Theorem znbas

Description: The base set of Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znbas.s ⊢ S = RSpan ⁡ ℤ ring
znbas.y ⊢ Y = ℤ/Nℤ
znbas.r ⊢ R = ℤ ring ~ QG S ⁡ N
Assertion znbas ⊢ N ∈ ℕ 0 → ℤ / R = Base Y

Proof

Step Hyp Ref Expression
1 znbas.s ⊢ S = RSpan ⁡ ℤ ring
2 znbas.y ⊢ Y = ℤ/Nℤ
3 znbas.r ⊢ R = ℤ ring ~ QG S ⁡ N
4 eqidd ⊢ N ∈ ℕ 0 → ℤ ring / 𝑠 R = ℤ ring / 𝑠 R
5 zringbas ⊢ ℤ = Base ℤ ring
6 5 a1i ⊢ N ∈ ℕ 0 → ℤ = Base ℤ ring
7 3 ovexi ⊢ R ∈ V
8 7 a1i ⊢ N ∈ ℕ 0 → R ∈ V
9 zringring ⊢ ℤ ring ∈ Ring
10 9 a1i ⊢ N ∈ ℕ 0 → ℤ ring ∈ Ring
11 4 6 8 10 qusbas ⊢ N ∈ ℕ 0 → ℤ / R = Base ℤ ring / 𝑠 R
12 3 oveq2i ⊢ ℤ ring / 𝑠 R = ℤ ring / 𝑠 ℤ ring ~ QG S ⁡ N
13 1 12 2 znbas2 ⊢ N ∈ ℕ 0 → Base ℤ ring / 𝑠 R = Base Y
14 11 13 eqtrd ⊢ N ∈ ℕ 0 → ℤ / R = Base Y