Theorem 0ringcring

Description: The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	0ringcring.1	$$⊢B={\mathrm{Base}}_R$$
	0ringcring.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	0ringcring.3	$$⊢\phi \to \left|B\right|=1$$
Assertion	0ringcring	$$⊢\phi \to R\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		0ringcring.1	$$⊢B={\mathrm{Base}}_R$$
2		0ringcring.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		0ringcring.3	$$⊢\phi \to \left|B\right|=1$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5	4 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
6	5	a1i	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8	4 7	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
9	8	a1i	$$⊢\phi \to {\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
10	4	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
11	2 10	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
12		eqid	$$⊢0_R=0_R$$
13	2	3ad2ant1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to R\in \mathrm{Ring}$$
14		simp3	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to y\in B$$
15	1 7 12 13 14	ringlzd	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to 0_R{\cdot }_{R}y=0_R$$
16	1 7 12 13 14	ringrzd	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to y{\cdot }_R{0}_R=0_R$$
17	15 16	eqtr4d	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to 0_R{\cdot }_{R}y=y{\cdot }_R{0}_R$$
18		simp2	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\in B$$
19	1 12	0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to B=\left\{0_R\right\}$$
20	2 3 19	syl2anc	$$⊢\phi \to B=\left\{0_R\right\}$$
21	20	3ad2ant1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to B=\left\{0_R\right\}$$
22	18 21	eleqtrd	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\in \left\{0_R\right\}$$
23		elsni	$$⊢x\in \left\{0_R\right\}\to x=0_R$$
24	22 23	syl	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x=0_R$$
25	24	oveq1d	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x{\cdot }_{R}y=0_R{\cdot }_{R}y$$
26	24	oveq2d	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to y{\cdot }_{R}x=y{\cdot }_R{0}_R$$
27	17 25 26	3eqtr4d	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x{\cdot }_{R}y=y{\cdot }_{R}x$$
28	6 9 11 27	iscmnd	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{CMnd}$$
29	4	iscrng	$$⊢R\in \mathrm{CRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R\in \mathrm{CMnd}\right)$$
30	2 28 29	sylanbrc	$$⊢\phi \to R\in \mathrm{CRing}$$