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 ) |