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

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 )