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