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 𝑂 = ( oppr𝑅 )
Assertion opprdrng ( 𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 opprdrng.1 𝑂 = ( oppr𝑅 )
2 1 opprringb ( 𝑅 ∈ Ring ↔ 𝑂 ∈ Ring )
3 2 anbi1i ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g𝑅 ) } ) ) ↔ ( 𝑂 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g𝑅 ) } ) ) )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
6 eqid ( 0g𝑅 ) = ( 0g𝑅 )
7 4 5 6 isdrng ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g𝑅 ) } ) ) )
8 1 4 opprbas ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
9 5 1 opprunit ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑂 )
10 1 6 oppr0 ( 0g𝑅 ) = ( 0g𝑂 )
11 8 9 10 isdrng ( 𝑂 ∈ DivRing ↔ ( 𝑂 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g𝑅 ) } ) ) )
12 3 7 11 3bitr4i ( 𝑅 ∈ DivRing ↔ 𝑂 ∈ DivRing )