Theorem iscrngd

Description: Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	isringd.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
	isringd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_R$$
	isringd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
	isringd.g	$$⊢\phi \to R\in \mathrm{Grp}$$
	isringd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{·}y\in B$$
	isringd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
	isringd.d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
	isringd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
	isringd.u	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
	isringd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
	isringd.h	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{·}\underset{\dot{}}{1}=x$$
	iscrngd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{·}y=y\underset{\dot{}}{·}x$$
Assertion	iscrngd	$$⊢\phi \to R\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		isringd.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		isringd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_R$$
3		isringd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
4		isringd.g	$$⊢\phi \to R\in \mathrm{Grp}$$
5		isringd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{·}y\in B$$
6		isringd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
7		isringd.d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
8		isringd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
9		isringd.u	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
10		isringd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
11		isringd.h	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{·}\underset{\dot{}}{1}=x$$
12		iscrngd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{·}y=y\underset{\dot{}}{·}x$$
13	1 2 3 4 5 6 7 8 9 10 11	isringd	$$⊢\phi \to R\in \mathrm{Ring}$$
14		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16	14 15	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
17	1 16	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
18		eqid	$$⊢{\cdot }_R={\cdot }_R$$
19	14 18	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
20	3 19	eqtrdi	$$⊢\phi \to \underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
21	17 20 5 6 9 10 11	ismndd	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
22	17 20 21 12	iscmnd	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{CMnd}$$
23	14	iscrng	$$⊢R\in \mathrm{CRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_R\in \mathrm{CMnd}\right)$$
24	13 22 23	sylanbrc	$$⊢\phi \to R\in \mathrm{CRing}$$