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=oppr⁡R
Assertion opprsubrg ⊢SubRing⁡R=SubRing⁡O

Proof

Step Hyp Ref Expression
1 opprsubrg.o ⊢O=oppr⁡R
2 subrgrcl ⊢x∈SubRing⁡R→R∈Ring
3 subrgrcl ⊢x∈SubRing⁡O→O∈Ring
4 1 opprringb ⊢R∈Ring↔O∈Ring
5 3 4 sylibr ⊢x∈SubRing⁡O→R∈Ring
6 1 opprsubg ⊢SubGrp⁡R=SubGrp⁡O
7 6 a1i ⊢R∈Ring→SubGrp⁡R=SubGrp⁡O
8 7 eleq2d ⊢R∈Ring→x∈SubGrp⁡R↔x∈SubGrp⁡O
9 ralcom ⊢∀y∈x∀z∈xy⋅Rz∈x↔∀z∈x∀y∈xy⋅Rz∈x
10 eqid ⊢BaseR=BaseR
11 eqid ⊢⋅R=⋅R
12 eqid ⊢⋅O=⋅O
13 10 11 1 12 opprmul ⊢z⋅Oy=y⋅Rz
14 13 eleq1i ⊢z⋅Oy∈x↔y⋅Rz∈x
15 14 2ralbii ⊢∀z∈x∀y∈xz⋅Oy∈x↔∀z∈x∀y∈xy⋅Rz∈x
16 9 15 bitr4i ⊢∀y∈x∀z∈xy⋅Rz∈x↔∀z∈x∀y∈xz⋅Oy∈x
17 16 a1i ⊢R∈Ring→∀y∈x∀z∈xy⋅Rz∈x↔∀z∈x∀y∈xz⋅Oy∈x
18 8 17 3anbi13d ⊢R∈Ring→x∈SubGrp⁡R∧1R∈x∧∀y∈x∀z∈xy⋅Rz∈x↔x∈SubGrp⁡O∧1R∈x∧∀z∈x∀y∈xz⋅Oy∈x
19 eqid ⊢1R=1R
20 10 19 11 issubrg2 ⊢R∈Ring→x∈SubRing⁡R↔x∈SubGrp⁡R∧1R∈x∧∀y∈x∀z∈xy⋅Rz∈x
21 1 10 opprbas ⊢BaseR=BaseO
22 1 19 oppr1 ⊢1R=1O
23 21 22 12 issubrg2 ⊢O∈Ring→x∈SubRing⁡O↔x∈SubGrp⁡O∧1R∈x∧∀z∈x∀y∈xz⋅Oy∈x
24 4 23 sylbi ⊢R∈Ring→x∈SubRing⁡O↔x∈SubGrp⁡O∧1R∈x∧∀z∈x∀y∈xz⋅Oy∈x
25 18 20 24 3bitr4d ⊢R∈Ring→x∈SubRing⁡R↔x∈SubRing⁡O
26 2 5 25 pm5.21nii ⊢x∈SubRing⁡R↔x∈SubRing⁡O
27 26 eqriv ⊢SubRing⁡R=SubRing⁡O