Metamath Proof Explorer

Theorem drngpropd

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

Ref Expression
Hypotheses drngpropd.1 ⊢ φ → B = Base K
drngpropd.2 ⊢ φ → B = Base L
drngpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
drngpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
Assertion drngpropd ⊢ φ → K ∈ DivRing ↔ L ∈ DivRing

Proof

Step Hyp Ref Expression
1 drngpropd.1 ⊢ φ → B = Base K
2 drngpropd.2 ⊢ φ → B = Base L
3 drngpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 drngpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
5 1 2 4 unitpropd ⊢ φ → Unit ⁡ K = Unit ⁡ L
6 5 adantr ⊢ φ ∧ K ∈ Ring → Unit ⁡ K = Unit ⁡ L
7 1 2 eqtr3d ⊢ φ → Base K = Base L
8 7 adantr ⊢ φ ∧ K ∈ Ring → Base K = Base L
9 1 adantr ⊢ φ ∧ K ∈ Ring → B = Base K
10 2 adantr ⊢ φ ∧ K ∈ Ring → B = Base L
11 3 adantlr ⊢ φ ∧ K ∈ Ring ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
12 9 10 11 grpidpropd ⊢ φ ∧ K ∈ Ring → 0 K = 0 L
13 12 sneqd ⊢ φ ∧ K ∈ Ring → 0 K = 0 L
14 8 13 difeq12d ⊢ φ ∧ K ∈ Ring → Base K ∖ 0 K = Base L ∖ 0 L
15 6 14 eqeq12d ⊢ φ ∧ K ∈ Ring → Unit ⁡ K = Base K ∖ 0 K ↔ Unit ⁡ L = Base L ∖ 0 L
16 15 pm5.32da ⊢ φ → K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K ↔ K ∈ Ring ∧ Unit ⁡ L = Base L ∖ 0 L
17 1 2 3 4 ringpropd ⊢ φ → K ∈ Ring ↔ L ∈ Ring
18 17 anbi1d ⊢ φ → K ∈ Ring ∧ Unit ⁡ L = Base L ∖ 0 L ↔ L ∈ Ring ∧ Unit ⁡ L = Base L ∖ 0 L
19 16 18 bitrd ⊢ φ → K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K ↔ L ∈ Ring ∧ Unit ⁡ L = Base L ∖ 0 L
20 eqid ⊢ Base K = Base K
21 eqid ⊢ Unit ⁡ K = Unit ⁡ K
22 eqid ⊢ 0 K = 0 K
23 20 21 22 isdrng ⊢ K ∈ DivRing ↔ K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K
24 eqid ⊢ Base L = Base L
25 eqid ⊢ Unit ⁡ L = Unit ⁡ L
26 eqid ⊢ 0 L = 0 L
27 24 25 26 isdrng ⊢ L ∈ DivRing ↔ L ∈ Ring ∧ Unit ⁡ L = Base L ∖ 0 L
28 19 23 27 3bitr4g ⊢ φ → K ∈ DivRing ↔ L ∈ DivRing