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 ⊢ 𝑆 = ( RSpan ‘ ℤring )
znbas.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znbas.r ⊢ 𝑅 = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
Assertion znbas ( 𝑁 ∈ ℕ0 → ( ℤ / 𝑅 ) = ( Base ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 znbas.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
2 znbas.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
3 znbas.r ⊢ 𝑅 = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) )
4 eqidd ⊢ ( 𝑁 ∈ ℕ0 → ( ℤring /s 𝑅 ) = ( ℤring /s 𝑅 ) )
5 zringbas ⊢ ℤ = ( Base ‘ ℤring )
6 5 a1i ⊢ ( 𝑁 ∈ ℕ0 → ℤ = ( Base ‘ ℤring ) )
7 3 ovexi ⊢ 𝑅 ∈ V
8 7 a1i ⊢ ( 𝑁 ∈ ℕ0 → 𝑅 ∈ V )
9 zringring ⊢ ℤring ∈ Ring
10 9 a1i ⊢ ( 𝑁 ∈ ℕ0 → ℤring ∈ Ring )
11 4 6 8 10 qusbas ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / 𝑅 ) = ( Base ‘ ( ℤring /s 𝑅 ) ) )
12 3 oveq2i ⊢ ( ℤring /s 𝑅 ) = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
13 1 12 2 znbas2 ⊢ ( 𝑁 ∈ ℕ0 → ( Base ‘ ( ℤring /s 𝑅 ) ) = ( Base ‘ 𝑌 ) )
14 11 13 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ / 𝑅 ) = ( Base ‘ 𝑌 ) )