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	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	cznrng.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	cznrng.x	⊢ 𝑋 = ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ )
Assertion	cznrnglem	⊢ 𝐵 = ( Base ‘ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cznrng.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2		cznrng.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		cznrng.x	⊢ 𝑋 = ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ )
4		baseid	⊢ Base = Slot ( Base ‘ ndx )
5		basendxnmulrndx	⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
6	4 5	setsnid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
7	3	eqcomi	⊢ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) = 𝑋
8	7	fveq2i	⊢ ( Base ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) ) = ( Base ‘ 𝑋 )
9	2 6 8	3eqtri	⊢ 𝐵 = ( Base ‘ 𝑋 )