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 e. ( SubRing ` R ) -> R e. Ring )
3 subrgrcl 
 |-  ( x e. ( SubRing ` O ) -> O e. Ring )
4 1 opprringb 
 |-  ( R e. Ring <-> O e. Ring )
5 3 4 sylibr 
 |-  ( x e. ( SubRing ` O ) -> R e. Ring )
6 1 opprsubg 
 |-  ( SubGrp ` R ) = ( SubGrp ` O )
7 6 a1i 
 |-  ( R e. Ring -> ( SubGrp ` R ) = ( SubGrp ` O ) )
8 7 eleq2d 
 |-  ( R e. Ring -> ( x e. ( SubGrp ` R ) <-> x e. ( SubGrp ` O ) ) )
9 ralcom 
 |-  ( A. y e. x A. z e. x ( y ( .r ` R ) z ) e. x <-> A. z e. x A. y e. x ( y ( .r ` R ) z ) e. x )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 eqid 
 |-  ( .r ` O ) = ( .r ` O )
13 10 11 1 12 opprmul 
 |-  ( z ( .r ` O ) y ) = ( y ( .r ` R ) z )
14 13 eleq1i 
 |-  ( ( z ( .r ` O ) y ) e. x <-> ( y ( .r ` R ) z ) e. x )
15 14 2ralbii 
 |-  ( A. z e. x A. y e. x ( z ( .r ` O ) y ) e. x <-> A. z e. x A. y e. x ( y ( .r ` R ) z ) e. x )
16 9 15 bitr4i 
 |-  ( A. y e. x A. z e. x ( y ( .r ` R ) z ) e. x <-> A. z e. x A. y e. x ( z ( .r ` O ) y ) e. x )
17 16 a1i 
 |-  ( R e. Ring -> ( A. y e. x A. z e. x ( y ( .r ` R ) z ) e. x <-> A. z e. x A. y e. x ( z ( .r ` O ) y ) e. x ) )
18 8 17 3anbi13d 
 |-  ( R e. Ring -> ( ( x e. ( SubGrp ` R ) /\ ( 1r ` R ) e. x /\ A. y e. x A. z e. x ( y ( .r ` R ) z ) e. x ) <-> ( x e. ( SubGrp ` O ) /\ ( 1r ` R ) e. x /\ A. z e. x A. y e. x ( z ( .r ` O ) y ) e. x ) ) )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 10 19 11 issubrg2 
 |-  ( R e. Ring -> ( x e. ( SubRing ` R ) <-> ( x e. ( SubGrp ` R ) /\ ( 1r ` R ) e. x /\ A. y e. x A. z e. x ( y ( .r ` R ) z ) e. x ) ) )
21 1 10 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
22 1 19 oppr1 
 |-  ( 1r ` R ) = ( 1r ` O )
23 21 22 12 issubrg2 
 |-  ( O e. Ring -> ( x e. ( SubRing ` O ) <-> ( x e. ( SubGrp ` O ) /\ ( 1r ` R ) e. x /\ A. z e. x A. y e. x ( z ( .r ` O ) y ) e. x ) ) )
24 4 23 sylbi 
 |-  ( R e. Ring -> ( x e. ( SubRing ` O ) <-> ( x e. ( SubGrp ` O ) /\ ( 1r ` R ) e. x /\ A. z e. x A. y e. x ( z ( .r ` O ) y ) e. x ) ) )
25 18 20 24 3bitr4d 
 |-  ( R e. Ring -> ( x e. ( SubRing ` R ) <-> x e. ( SubRing ` O ) ) )
26 2 5 25 pm5.21nii 
 |-  ( x e. ( SubRing ` R ) <-> x e. ( SubRing ` O ) )
27 26 eqriv 
 |-  ( SubRing ` R ) = ( SubRing ` O )