Metamath Proof Explorer

Theorem opprdrng

Description: The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypothesis opprdrng.1 ⊢ O = opp r ⁡ R
Assertion opprdrng ⊢ R ∈ DivRing ↔ O ∈ DivRing

Proof

Step Hyp Ref Expression
1 opprdrng.1 ⊢ O = opp r ⁡ R
2 1 opprringb ⊢ R ∈ Ring ↔ O ∈ Ring
3 2 anbi1i ⊢ R ∈ Ring ∧ Unit ⁡ R = Base R ∖ 0 R ↔ O ∈ Ring ∧ Unit ⁡ R = Base R ∖ 0 R
4 eqid ⊢ Base R = Base R
5 eqid ⊢ Unit ⁡ R = Unit ⁡ R
6 eqid ⊢ 0 R = 0 R
7 4 5 6 isdrng ⊢ R ∈ DivRing ↔ R ∈ Ring ∧ Unit ⁡ R = Base R ∖ 0 R
8 1 4 opprbas ⊢ Base R = Base O
9 5 1 opprunit ⊢ Unit ⁡ R = Unit ⁡ O
10 1 6 oppr0 ⊢ 0 R = 0 O
11 8 9 10 isdrng ⊢ O ∈ DivRing ↔ O ∈ Ring ∧ Unit ⁡ R = Base R ∖ 0 R
12 3 7 11 3bitr4i ⊢ R ∈ DivRing ↔ O ∈ DivRing