Metamath Proof Explorer

Theorem opprsubrng

Description: Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypothesis opprsubrng.o 
|- O = ( oppR ` R )
Assertion opprsubrng 
|- ( SubRng ` R ) = ( SubRng ` O )

Proof

Step Hyp Ref Expression
1 opprsubrng.o 
 |-  O = ( oppR ` R )
2 subrngrcl 
 |-  ( x e. ( SubRng ` R ) -> R e. Rng )
3 subrngrcl 
 |-  ( x e. ( SubRng ` O ) -> O e. Rng )
4 1 opprrngb 
 |-  ( R e. Rng <-> O e. Rng )
5 3 4 sylibr 
 |-  ( x e. ( SubRng ` O ) -> R e. Rng )
6 1 opprsubg 
 |-  ( SubGrp ` R ) = ( SubGrp ` O )
7 6 a1i 
 |-  ( R e. Rng -> ( SubGrp ` R ) = ( SubGrp ` O ) )
8 7 eleq2d 
 |-  ( R e. Rng -> ( x e. ( SubGrp ` R ) <-> x e. ( SubGrp ` O ) ) )
9 ralcom 
 |-  ( A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x <-> A. y e. x A. z e. x ( z ( .r ` R ) y ) 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 
 |-  ( y ( .r ` O ) z ) = ( z ( .r ` R ) y )
14 13 eleq1i 
 |-  ( ( y ( .r ` O ) z ) e. x <-> ( z ( .r ` R ) y ) e. x )
15 14 2ralbii 
 |-  ( A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x <-> A. y e. x A. z e. x ( z ( .r ` R ) y ) e. x )
16 9 15 bitr4i 
 |-  ( A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x <-> A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x )
17 16 a1i 
 |-  ( R e. Rng -> ( A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x <-> A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) )
18 8 17 anbi12d 
 |-  ( R e. Rng -> ( ( x e. ( SubGrp ` R ) /\ A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) )
19 10 11 issubrng2 
 |-  ( R e. Rng -> ( x e. ( SubRng ` R ) <-> ( x e. ( SubGrp ` R ) /\ A. z e. x A. y e. x ( z ( .r ` R ) y ) e. x ) ) )
20 1 10 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
21 20 12 issubrng2 
 |-  ( O e. Rng -> ( x e. ( SubRng ` O ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) )
22 4 21 sylbi 
 |-  ( R e. Rng -> ( x e. ( SubRng ` O ) <-> ( x e. ( SubGrp ` O ) /\ A. y e. x A. z e. x ( y ( .r ` O ) z ) e. x ) ) )
23 18 19 22 3bitr4d 
 |-  ( R e. Rng -> ( x e. ( SubRng ` R ) <-> x e. ( SubRng ` O ) ) )
24 2 5 23 pm5.21nii 
 |-  ( x e. ( SubRng ` R ) <-> x e. ( SubRng ` O ) )
25 24 eqriv 
 |-  ( SubRng ` R ) = ( SubRng ` O )