# Metamath Proof Explorer

## Theorem opprsubrg

Description: Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014)

Ref Expression
Hypothesis opprsubrg.o ${⊢}{O}={opp}_{r}\left({R}\right)$
Assertion opprsubrg ${⊢}\mathrm{SubRing}\left({R}\right)=\mathrm{SubRing}\left({O}\right)$

### Proof

Step Hyp Ref Expression
1 opprsubrg.o ${⊢}{O}={opp}_{r}\left({R}\right)$
2 subrgrcl ${⊢}{x}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
3 subrgrcl ${⊢}{x}\in \mathrm{SubRing}\left({O}\right)\to {O}\in \mathrm{Ring}$
4 1 opprringb ${⊢}{R}\in \mathrm{Ring}↔{O}\in \mathrm{Ring}$
5 3 4 sylibr ${⊢}{x}\in \mathrm{SubRing}\left({O}\right)\to {R}\in \mathrm{Ring}$
6 1 opprsubg ${⊢}\mathrm{SubGrp}\left({R}\right)=\mathrm{SubGrp}\left({O}\right)$
7 6 a1i ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubGrp}\left({R}\right)=\mathrm{SubGrp}\left({O}\right)$
8 7 eleq2d ${⊢}{R}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubGrp}\left({R}\right)↔{x}\in \mathrm{SubGrp}\left({O}\right)\right)$
9 ralcom ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}$
10 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
11 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
12 eqid ${⊢}{\cdot }_{{O}}={\cdot }_{{O}}$
13 10 11 1 12 opprmul ${⊢}{z}{\cdot }_{{O}}{y}={y}{\cdot }_{{R}}{z}$
14 13 eleq1i ${⊢}{z}{\cdot }_{{O}}{y}\in {x}↔{y}{\cdot }_{{R}}{z}\in {x}$
15 14 2ralbii ${⊢}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{O}}{y}\in {x}↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}$
16 9 15 bitr4i ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{O}}{y}\in {x}$
17 16 a1i ${⊢}{R}\in \mathrm{Ring}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}↔\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{O}}{y}\in {x}\right)$
18 8 17 3anbi13d ${⊢}{R}\in \mathrm{Ring}\to \left(\left({x}\in \mathrm{SubGrp}\left({R}\right)\wedge {1}_{{R}}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}\right)↔\left({x}\in \mathrm{SubGrp}\left({O}\right)\wedge {1}_{{R}}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{O}}{y}\in {x}\right)\right)$
19 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
20 10 19 11 issubrg2 ${⊢}{R}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubRing}\left({R}\right)↔\left({x}\in \mathrm{SubGrp}\left({R}\right)\wedge {1}_{{R}}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\forall {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{{R}}{z}\in {x}\right)\right)$
21 1 10 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{O}}$
22 1 19 oppr1 ${⊢}{1}_{{R}}={1}_{{O}}$
23 21 22 12 issubrg2 ${⊢}{O}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubRing}\left({O}\right)↔\left({x}\in \mathrm{SubGrp}\left({O}\right)\wedge {1}_{{R}}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{O}}{y}\in {x}\right)\right)$
24 4 23 sylbi ${⊢}{R}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubRing}\left({O}\right)↔\left({x}\in \mathrm{SubGrp}\left({O}\right)\wedge {1}_{{R}}\in {x}\wedge \forall {z}\in {x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{{O}}{y}\in {x}\right)\right)$
25 18 20 24 3bitr4d ${⊢}{R}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubRing}\left({R}\right)↔{x}\in \mathrm{SubRing}\left({O}\right)\right)$
26 2 5 25 pm5.21nii ${⊢}{x}\in \mathrm{SubRing}\left({R}\right)↔{x}\in \mathrm{SubRing}\left({O}\right)$
27 26 eqriv ${⊢}\mathrm{SubRing}\left({R}\right)=\mathrm{SubRing}\left({O}\right)$