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

Proof

Step Hyp Ref Expression
1 opprsubrg.o O = opp r 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 x y R z x z x y x y R z x
10 eqid Base R = Base R
11 eqid R = R
12 eqid O = O
13 10 11 1 12 opprmul z O y = y R z
14 13 eleq1i z O y x y R z x
15 14 2ralbii z x y x z O y x z x y x y R z x
16 9 15 bitr4i y x z x y R z x z x y x z O y x
17 16 a1i R Ring y x z x y R z x z x y x z O y x
18 8 17 3anbi13d R Ring x SubGrp R 1 R x y x z x y R z x x SubGrp O 1 R x z x y x z O y x
19 eqid 1 R = 1 R
20 10 19 11 issubrg2 R Ring x SubRing R x SubGrp R 1 R x y x z x y R z x
21 1 10 opprbas Base R = Base O
22 1 19 oppr1 1 R = 1 O
23 21 22 12 issubrg2 O Ring x SubRing O x SubGrp O 1 R x z x y x z O y x
24 4 23 sylbi R Ring x SubRing O x SubGrp O 1 R x z x y x z O y 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