# Metamath Proof Explorer

## 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}↔{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}↔{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 syl6eq ${⊢}{\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 syl6eq ${⊢}{\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}↔{\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)↔\left({L}\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_{{L}}\in \mathrm{CMnd}\right)\right)$
23 6 iscrng ${⊢}{K}\in \mathrm{CRing}↔\left({K}\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_{{K}}\in \mathrm{CMnd}\right)$
24 10 iscrng ${⊢}{L}\in \mathrm{CRing}↔\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}↔{L}\in \mathrm{CRing}\right)$