Theorem crngpropd

Description: If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	ringpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	ringpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	ringpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	ringpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	crngpropd	$$⊢\phi \to \left(K\in \mathrm{CRing}\leftrightarrow L\in \mathrm{CRing}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		ringpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		ringpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4		ringpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
5	1 2 3 4	ringpropd	$$⊢\phi \to \left(K\in \mathrm{Ring}\leftrightarrow L\in \mathrm{Ring}\right)$$
6		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
7		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
8	6 7	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
9	1 8	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
10		eqid	$$⊢{\mathrm{mulGrp}}_L={\mathrm{mulGrp}}_L$$
11		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
12	10 11	mgpbas	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
13	2 12	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
14		eqid	$$⊢{\cdot }_K={\cdot }_K$$
15	6 14	mgpplusg	$$⊢{\cdot }_K={+}_{{\mathrm{mulGrp}}_K}$$
16	15	oveqi	$$⊢x{\cdot }_{K}y=x{+}_{{\mathrm{mulGrp}}_K}y$$
17		eqid	$$⊢{\cdot }_L={\cdot }_L$$
18	10 17	mgpplusg	$$⊢{\cdot }_L={+}_{{\mathrm{mulGrp}}_L}$$
19	18	oveqi	$$⊢x{\cdot }_{L}y=x{+}_{{\mathrm{mulGrp}}_L}y$$
20	4 16 19	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{{\mathrm{mulGrp}}_K}y=x{+}_{{\mathrm{mulGrp}}_L}y$$
21	9 13 20	cmnpropd	$$⊢\phi \to \left({\mathrm{mulGrp}}_K\in \mathrm{CMnd}\leftrightarrow {\mathrm{mulGrp}}_L\in \mathrm{CMnd}\right)$$
22	5 21	anbi12d	$$⊢\phi \to \left(\left(K\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_K\in \mathrm{CMnd}\right)\leftrightarrow \left(L\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_L\in \mathrm{CMnd}\right)\right)$$
23	6	iscrng	$$⊢K\in \mathrm{CRing}\leftrightarrow \left(K\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_K\in \mathrm{CMnd}\right)$$
24	10	iscrng	$$⊢L\in \mathrm{CRing}\leftrightarrow \left(L\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_L\in \mathrm{CMnd}\right)$$
25	22 23 24	3bitr4g	$$⊢\phi \to \left(K\in \mathrm{CRing}\leftrightarrow L\in \mathrm{CRing}\right)$$