Metamath Proof Explorer

Theorem oppgsubg

Description: Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis oppggic.o 
|- O = ( oppG ` G )
Assertion oppgsubg 
|- ( SubGrp ` G ) = ( SubGrp ` O )

Proof

Step Hyp Ref Expression
1 oppggic.o 
 |-  O = ( oppG ` G )
2 subgrcl 
 |-  ( x e. ( SubGrp ` G ) -> G e. Grp )
3 subgrcl 
 |-  ( x e. ( SubGrp ` O ) -> O e. Grp )
4 1 oppggrpb 
 |-  ( G e. Grp <-> O e. Grp )
5 3 4 sylibr 
 |-  ( x e. ( SubGrp ` O ) -> G e. Grp )
6 1 oppgsubm 
 |-  ( SubMnd ` G ) = ( SubMnd ` O )
7 6 eleq2i 
 |-  ( x e. ( SubMnd ` G ) <-> x e. ( SubMnd ` O ) )
8 7 a1i 
 |-  ( G e. Grp -> ( x e. ( SubMnd ` G ) <-> x e. ( SubMnd ` O ) ) )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 1 9 oppginv 
 |-  ( G e. Grp -> ( invg ` G ) = ( invg ` O ) )
11 10 fveq1d 
 |-  ( G e. Grp -> ( ( invg ` G ) ` y ) = ( ( invg ` O ) ` y ) )
12 11 eleq1d 
 |-  ( G e. Grp -> ( ( ( invg ` G ) ` y ) e. x <-> ( ( invg ` O ) ` y ) e. x ) )
13 12 ralbidv 
 |-  ( G e. Grp -> ( A. y e. x ( ( invg ` G ) ` y ) e. x <-> A. y e. x ( ( invg ` O ) ` y ) e. x ) )
14 8 13 anbi12d 
 |-  ( G e. Grp -> ( ( x e. ( SubMnd ` G ) /\ A. y e. x ( ( invg ` G ) ` y ) e. x ) <-> ( x e. ( SubMnd ` O ) /\ A. y e. x ( ( invg ` O ) ` y ) e. x ) ) )
15 9 issubg3 
 |-  ( G e. Grp -> ( x e. ( SubGrp ` G ) <-> ( x e. ( SubMnd ` G ) /\ A. y e. x ( ( invg ` G ) ` y ) e. x ) ) )
16 eqid 
 |-  ( invg ` O ) = ( invg ` O )
17 16 issubg3 
 |-  ( O e. Grp -> ( x e. ( SubGrp ` O ) <-> ( x e. ( SubMnd ` O ) /\ A. y e. x ( ( invg ` O ) ` y ) e. x ) ) )
18 4 17 sylbi 
 |-  ( G e. Grp -> ( x e. ( SubGrp ` O ) <-> ( x e. ( SubMnd ` O ) /\ A. y e. x ( ( invg ` O ) ` y ) e. x ) ) )
19 14 15 18 3bitr4d 
 |-  ( G e. Grp -> ( x e. ( SubGrp ` G ) <-> x e. ( SubGrp ` O ) ) )
20 2 5 19 pm5.21nii 
 |-  ( x e. ( SubGrp ` G ) <-> x e. ( SubGrp ` O ) )
21 20 eqriv 
 |-  ( SubGrp ` G ) = ( SubGrp ` O )