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=\mathbb{Z}/N\mathbb{Z}$$
	cznrng.b	$$⊢B={\mathrm{Base}}_Y$$
	cznrng.x	$$⊢X=Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩$$
Assertion	cznrnglem	$$⊢B={\mathrm{Base}}_X$$

Proof

Step	Hyp	Ref	Expression
1		cznrng.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		cznrng.b	$$⊢B={\mathrm{Base}}_Y$$
3		cznrng.x	$$⊢X=Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩$$
4		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
6	4 5	setsnid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
7	3	eqcomi	$$⊢Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩=X$$
8	7	fveq2i	$$⊢{\mathrm{Base}}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}={\mathrm{Base}}_X$$
9	2 6 8	3eqtri	$$⊢B={\mathrm{Base}}_X$$