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 φ B = Base K
ringpropd.2 φ B = Base L
ringpropd.3 φ x B y B x + K y = x + L y
ringpropd.4 φ x B y B x K y = x L y
Assertion crngpropd φ K CRing L CRing

Proof

Step Hyp Ref Expression
1 ringpropd.1 φ B = Base K
2 ringpropd.2 φ B = Base L
3 ringpropd.3 φ x B y B x + K y = x + L y
4 ringpropd.4 φ x B y B x K y = x L y
5 1 2 3 4 ringpropd φ K Ring L Ring
6 eqid mulGrp K = mulGrp K
7 eqid Base K = Base K
8 6 7 mgpbas Base K = Base mulGrp K
9 1 8 syl6eq φ B = Base mulGrp K
10 eqid mulGrp L = mulGrp L
11 eqid Base L = Base L
12 10 11 mgpbas Base L = Base mulGrp L
13 2 12 syl6eq φ B = Base mulGrp L
14 eqid K = K
15 6 14 mgpplusg K = + mulGrp K
16 15 oveqi x K y = x + mulGrp K y
17 eqid L = L
18 10 17 mgpplusg L = + mulGrp L
19 18 oveqi x L y = x + mulGrp L y
20 4 16 19 3eqtr3g φ x B y B x + mulGrp K y = x + mulGrp L y
21 9 13 20 cmnpropd φ mulGrp K CMnd mulGrp L CMnd
22 5 21 anbi12d φ K Ring mulGrp K CMnd L Ring mulGrp L CMnd
23 6 iscrng K CRing K Ring mulGrp K CMnd
24 10 iscrng L CRing L Ring mulGrp L CMnd
25 22 23 24 3bitr4g φ K CRing L CRing