Metamath Proof Explorer


Theorem znbas2

Description: The base set of Z/nZ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-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 znbas2 ( 𝑁 ∈ ℕ0 → ( Base ‘ 𝑈 ) = ( Base ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 znval2.s 𝑆 = ( RSpan ‘ ℤring )
2 znval2.u 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3 znval2.y 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4 df-base Base = Slot 1
5 1nn 1 ∈ ℕ
6 1lt10 1 < 1 0
7 1 2 3 4 5 6 znbaslem ( 𝑁 ∈ ℕ0 → ( Base ‘ 𝑈 ) = ( Base ‘ 𝑌 ) )