Metamath Proof Explorer

Theorem opprsubg

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

Ref Expression
Hypothesis opprbas.1 
|- O = ( oppR ` R )
Assertion opprsubg 
|- ( SubGrp ` R ) = ( SubGrp ` O )

Proof

Step Hyp Ref Expression
1 opprbas.1 
 |-  O = ( oppR ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 1 2 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
4 eqid 
 |-  ( +g ` R ) = ( +g ` R )
5 1 4 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
6 3 5 grpprop 
 |-  ( R e. Grp <-> O e. Grp )
7 biid 
 |-  ( x C_ ( Base ` R ) <-> x C_ ( Base ` R ) )
8 eqid 
 |-  ( R |`s x ) = ( R |`s x )
9 8 2 ressbas 
 |-  ( x e. _V -> ( x i^i ( Base ` R ) ) = ( Base ` ( R |`s x ) ) )
10 9 elv 
 |-  ( x i^i ( Base ` R ) ) = ( Base ` ( R |`s x ) )
11 eqid 
 |-  ( O |`s x ) = ( O |`s x )
12 11 3 ressbas 
 |-  ( x e. _V -> ( x i^i ( Base ` R ) ) = ( Base ` ( O |`s x ) ) )
13 12 elv 
 |-  ( x i^i ( Base ` R ) ) = ( Base ` ( O |`s x ) )
14 10 13 eqtr3i 
 |-  ( Base ` ( R |`s x ) ) = ( Base ` ( O |`s x ) )
15 8 4 ressplusg 
 |-  ( x e. _V -> ( +g ` R ) = ( +g ` ( R |`s x ) ) )
16 11 5 ressplusg 
 |-  ( x e. _V -> ( +g ` R ) = ( +g ` ( O |`s x ) ) )
17 15 16 eqtr3d 
 |-  ( x e. _V -> ( +g ` ( R |`s x ) ) = ( +g ` ( O |`s x ) ) )
18 17 elv 
 |-  ( +g ` ( R |`s x ) ) = ( +g ` ( O |`s x ) )
19 14 18 grpprop 
 |-  ( ( R |`s x ) e. Grp <-> ( O |`s x ) e. Grp )
20 6 7 19 3anbi123i 
 |-  ( ( R e. Grp /\ x C_ ( Base ` R ) /\ ( R |`s x ) e. Grp ) <-> ( O e. Grp /\ x C_ ( Base ` R ) /\ ( O |`s x ) e. Grp ) )
21 2 issubg 
 |-  ( x e. ( SubGrp ` R ) <-> ( R e. Grp /\ x C_ ( Base ` R ) /\ ( R |`s x ) e. Grp ) )
22 3 issubg 
 |-  ( x e. ( SubGrp ` O ) <-> ( O e. Grp /\ x C_ ( Base ` R ) /\ ( O |`s x ) e. Grp ) )
23 20 21 22 3bitr4i 
 |-  ( x e. ( SubGrp ` R ) <-> x e. ( SubGrp ` O ) )
24 23 eqriv 
 |-  ( SubGrp ` R ) = ( SubGrp ` O )