Theorem cznrnglem

Description: Lemma for cznrng : The base set of the ring constructed from a Z/nZ structure by replacing the (multiplicative) ring operation by a constant operation is the base set of the Z/nZ structure. (Contributed by AV, 16-Feb-2020)

	Ref	Expression
Hypotheses	cznrng.y	|- Y = ( Z/nZ ` N )
	cznrng.b	|- B = ( Base ` Y )
	cznrng.x	|- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )
Assertion	cznrnglem	|- B = ( Base ` X )

Proof

Step	Hyp	Ref	Expression
1		cznrng.y	|- Y = ( Z/nZ ` N )
2		cznrng.b	|- B = ( Base ` Y )
3		cznrng.x	|- X = ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. )
4		baseid	|- Base = Slot ( Base ` ndx )
5		basendxnmulrndx	|- ( Base ` ndx ) =/= ( .r ` ndx )
6	4 5	setsnid	|- ( Base ` Y ) = ( Base ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) )
7	3	eqcomi	|- ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) = X
8	7	fveq2i	|- ( Base ` ( Y sSet <. ( .r ` ndx ) , ( x e. B , y e. B |-> C ) >. ) ) = ( Base ` X )
9	2 6 8	3eqtri	|- B = ( Base ` X )