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 ) )