Metamath Proof Explorer

Theorem drngprop

Description: If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013) (Revised by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses drngprop.b ⊢ Base K = Base L
drngprop.p ⊢ + K = + L
drngprop.m ⊢ ⋅ K = ⋅ L
Assertion drngprop ⊢ K ∈ DivRing ↔ L ∈ DivRing

Proof

Step Hyp Ref Expression
1 drngprop.b ⊢ Base K = Base L
2 drngprop.p ⊢ + K = + L
3 drngprop.m ⊢ ⋅ K = ⋅ L
4 eqidd ⊢ K ∈ Ring → Base K = Base K
5 1 a1i ⊢ K ∈ Ring → Base K = Base L
6 3 oveqi ⊢ x ⋅ K y = x ⋅ L y
7 6 a1i ⊢ K ∈ Ring ∧ x ∈ Base K ∧ y ∈ Base K → x ⋅ K y = x ⋅ L y
8 4 5 7 unitpropd ⊢ K ∈ Ring → Unit ⁡ K = Unit ⁡ L
9 2 oveqi ⊢ x + K y = x + L y
10 9 a1i ⊢ K ∈ Ring ∧ x ∈ Base K ∧ y ∈ Base K → x + K y = x + L y
11 4 5 10 grpidpropd ⊢ K ∈ Ring → 0 K = 0 L
12 11 sneqd ⊢ K ∈ Ring → 0 K = 0 L
13 12 difeq2d ⊢ K ∈ Ring → Base K ∖ 0 K = Base K ∖ 0 L
14 8 13 eqeq12d ⊢ K ∈ Ring → Unit ⁡ K = Base K ∖ 0 K ↔ Unit ⁡ L = Base K ∖ 0 L
15 14 pm5.32i ⊢ K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K ↔ K ∈ Ring ∧ Unit ⁡ L = Base K ∖ 0 L
16 1 2 3 ringprop ⊢ K ∈ Ring ↔ L ∈ Ring
17 16 anbi1i ⊢ K ∈ Ring ∧ Unit ⁡ L = Base K ∖ 0 L ↔ L ∈ Ring ∧ Unit ⁡ L = Base K ∖ 0 L
18 15 17 bitri ⊢ K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K ↔ L ∈ Ring ∧ Unit ⁡ L = Base K ∖ 0 L
19 eqid ⊢ Base K = Base K
20 eqid ⊢ Unit ⁡ K = Unit ⁡ K
21 eqid ⊢ 0 K = 0 K
22 19 20 21 isdrng ⊢ K ∈ DivRing ↔ K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K
23 eqid ⊢ Unit ⁡ L = Unit ⁡ L
24 eqid ⊢ 0 L = 0 L
25 1 23 24 isdrng ⊢ L ∈ DivRing ↔ L ∈ Ring ∧ Unit ⁡ L = Base K ∖ 0 L
26 18 22 25 3bitr4i ⊢ K ∈ DivRing ↔ L ∈ DivRing