Theorem cznabel

Description: The ring constructed from a Z/nZ structure by replacing the (multiplicative) ring operation by a constant operation is an abelian group. (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	cznabel	$$⊢\left(N\in \mathbb{N}\wedge C\in B\right)\to X\in \mathrm{Abel}$$

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		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
5	4	adantr	$$⊢\left(N\in \mathbb{N}\wedge C\in B\right)\to N\in {\mathbb{N}}_0$$
6	1	zncrng	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{CRing}$$
7	5 6	syl	$$⊢\left(N\in \mathbb{N}\wedge C\in B\right)\to Y\in \mathrm{CRing}$$
8		crngring	$$⊢Y\in \mathrm{CRing}\to Y\in \mathrm{Ring}$$
9		ringabl	$$⊢Y\in \mathrm{Ring}\to Y\in \mathrm{Abel}$$
10	7 8 9	3syl	$$⊢\left(N\in \mathbb{N}\wedge C\in B\right)\to Y\in \mathrm{Abel}$$
11	3	fveq2i	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
12		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
13		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
14	12 13	setsnid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
15	11 14	eqtr4i	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_Y$$
16	3	fveq2i	$$⊢{+}_X={+}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
17		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
18		plusgndxnmulrndx	$$⊢{+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
19	17 18	setsnid	$$⊢{+}_Y={+}_{\left(Y\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\left(x\in B,y\in B⟼C\right)⟩\right)}$$
20	16 19	eqtr4i	$$⊢{+}_X={+}_Y$$
21	15 20	ablprop	$$⊢X\in \mathrm{Abel}\leftrightarrow Y\in \mathrm{Abel}$$
22	10 21	sylibr	$$⊢\left(N\in \mathbb{N}\wedge C\in B\right)\to X\in \mathrm{Abel}$$