Metamath Proof Explorer


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=/N
cznrng.b B=BaseY
cznrng.x X=YsSetndxxB,yBC
Assertion cznrnglem B=BaseX

Proof

Step Hyp Ref Expression
1 cznrng.y Y=/N
2 cznrng.b B=BaseY
3 cznrng.x X=YsSetndxxB,yBC
4 baseid Base=SlotBasendx
5 basendxnmulrndx Basendxndx
6 4 5 setsnid BaseY=BaseYsSetndxxB,yBC
7 3 eqcomi YsSetndxxB,yBC=X
8 7 fveq2i BaseYsSetndxxB,yBC=BaseX
9 2 6 8 3eqtri B=BaseX