This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrdi ⊢ φ → 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 eqtrdi ⊢ φ → 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