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 ` ZZring )
znbas.y 
|- Y = ( Z/nZ ` N )
znbas.r 
|- R = ( ZZring ~QG ( S ` { N } ) )
Assertion znbas 
|- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )

Proof

Step Hyp Ref Expression
1 znbas.s 
 |-  S = ( RSpan ` ZZring )
2 znbas.y 
 |-  Y = ( Z/nZ ` N )
3 znbas.r 
 |-  R = ( ZZring ~QG ( S ` { N } ) )
4 eqidd 
 |-  ( N e. NN0 -> ( ZZring /s R ) = ( ZZring /s R ) )
5 zringbas 
 |-  ZZ = ( Base ` ZZring )
6 5 a1i 
 |-  ( N e. NN0 -> ZZ = ( Base ` ZZring ) )
7 3 ovexi 
 |-  R e. _V
8 7 a1i 
 |-  ( N e. NN0 -> R e. _V )
9 zringring 
 |-  ZZring e. Ring
10 9 a1i 
 |-  ( N e. NN0 -> ZZring e. Ring )
11 4 6 8 10 qusbas 
 |-  ( N e. NN0 -> ( ZZ /. R ) = ( Base ` ( ZZring /s R ) ) )
12 3 oveq2i 
 |-  ( ZZring /s R ) = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
13 1 12 2 znbas2 
 |-  ( N e. NN0 -> ( Base ` ( ZZring /s R ) ) = ( Base ` Y ) )
14 11 13 eqtrd 
 |-  ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )