# Metamath Proof Explorer

## Theorem opprringb

Description: Bidirectional form of opprring . (Contributed by Mario Carneiro, 6-Dec-2014)

Ref Expression
Hypothesis opprbas.1 ${⊢}{O}={opp}_{r}\left({R}\right)$
Assertion opprringb ${⊢}{R}\in \mathrm{Ring}↔{O}\in \mathrm{Ring}$

### Proof

Step Hyp Ref Expression
1 opprbas.1 ${⊢}{O}={opp}_{r}\left({R}\right)$
2 1 opprring ${⊢}{R}\in \mathrm{Ring}\to {O}\in \mathrm{Ring}$
3 eqid ${⊢}{opp}_{r}\left({O}\right)={opp}_{r}\left({O}\right)$
4 3 opprring ${⊢}{O}\in \mathrm{Ring}\to {opp}_{r}\left({O}\right)\in \mathrm{Ring}$
5 eqidd ${⊢}\top \to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
7 1 6 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{O}}$
8 3 7 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{opp}_{r}\left({O}\right)}$
9 8 a1i ${⊢}\top \to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{opp}_{r}\left({O}\right)}$
10 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
11 1 10 oppradd ${⊢}{+}_{{R}}={+}_{{O}}$
12 3 11 oppradd ${⊢}{+}_{{R}}={+}_{{opp}_{r}\left({O}\right)}$
13 12 oveqi ${⊢}{x}{+}_{{R}}{y}={x}{+}_{{opp}_{r}\left({O}\right)}{y}$
14 13 a1i ${⊢}\left(\top \wedge \left({x}\in {\mathrm{Base}}_{{R}}\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\right)\to {x}{+}_{{R}}{y}={x}{+}_{{opp}_{r}\left({O}\right)}{y}$
15 eqid ${⊢}{\cdot }_{{O}}={\cdot }_{{O}}$
16 eqid ${⊢}{\cdot }_{{opp}_{r}\left({O}\right)}={\cdot }_{{opp}_{r}\left({O}\right)}$
17 7 15 3 16 opprmul ${⊢}{x}{\cdot }_{{opp}_{r}\left({O}\right)}{y}={y}{\cdot }_{{O}}{x}$
18 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
19 6 18 1 15 opprmul ${⊢}{y}{\cdot }_{{O}}{x}={x}{\cdot }_{{R}}{y}$
20 17 19 eqtr2i ${⊢}{x}{\cdot }_{{R}}{y}={x}{\cdot }_{{opp}_{r}\left({O}\right)}{y}$
21 20 a1i ${⊢}\left(\top \wedge \left({x}\in {\mathrm{Base}}_{{R}}\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\right)\to {x}{\cdot }_{{R}}{y}={x}{\cdot }_{{opp}_{r}\left({O}\right)}{y}$
22 5 9 14 21 ringpropd ${⊢}\top \to \left({R}\in \mathrm{Ring}↔{opp}_{r}\left({O}\right)\in \mathrm{Ring}\right)$
23 22 mptru ${⊢}{R}\in \mathrm{Ring}↔{opp}_{r}\left({O}\right)\in \mathrm{Ring}$
24 4 23 sylibr ${⊢}{O}\in \mathrm{Ring}\to {R}\in \mathrm{Ring}$
25 2 24 impbii ${⊢}{R}\in \mathrm{Ring}↔{O}\in \mathrm{Ring}$