Metamath Proof Explorer

Theorem oppgsubm

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

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

Proof

Step Hyp Ref Expression
1 oppggic.o 
 |-  O = ( oppG ` G )
2 submrcl 
 |-  ( x e. ( SubMnd ` G ) -> G e. Mnd )
3 submrcl 
 |-  ( x e. ( SubMnd ` O ) -> O e. Mnd )
4 1 oppgmndb 
 |-  ( G e. Mnd <-> O e. Mnd )
5 3 4 sylibr 
 |-  ( x e. ( SubMnd ` O ) -> G e. Mnd )
6 ralcom 
 |-  ( A. y e. x A. z e. x ( y ( +g ` G ) z ) e. x <-> A. z e. x A. y e. x ( y ( +g ` G ) z ) e. x )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 eqid 
 |-  ( +g ` O ) = ( +g ` O )
9 7 1 8 oppgplus 
 |-  ( z ( +g ` O ) y ) = ( y ( +g ` G ) z )
10 9 eleq1i 
 |-  ( ( z ( +g ` O ) y ) e. x <-> ( y ( +g ` G ) z ) e. x )
11 10 2ralbii 
 |-  ( A. z e. x A. y e. x ( z ( +g ` O ) y ) e. x <-> A. z e. x A. y e. x ( y ( +g ` G ) z ) e. x )
12 6 11 bitr4i 
 |-  ( A. y e. x A. z e. x ( y ( +g ` G ) z ) e. x <-> A. z e. x A. y e. x ( z ( +g ` O ) y ) e. x )
13 12 3anbi3i 
 |-  ( ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. y e. x A. z e. x ( y ( +g ` G ) z ) e. x ) <-> ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. z e. x A. y e. x ( z ( +g ` O ) y ) e. x ) )
14 13 a1i 
 |-  ( G e. Mnd -> ( ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. y e. x A. z e. x ( y ( +g ` G ) z ) e. x ) <-> ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. z e. x A. y e. x ( z ( +g ` O ) y ) e. x ) ) )
15 eqid 
 |-  ( Base ` G ) = ( Base ` G )
16 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
17 15 16 7 issubm 
 |-  ( G e. Mnd -> ( x e. ( SubMnd ` G ) <-> ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. y e. x A. z e. x ( y ( +g ` G ) z ) e. x ) ) )
18 1 15 oppgbas 
 |-  ( Base ` G ) = ( Base ` O )
19 1 16 oppgid 
 |-  ( 0g ` G ) = ( 0g ` O )
20 18 19 8 issubm 
 |-  ( O e. Mnd -> ( x e. ( SubMnd ` O ) <-> ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. z e. x A. y e. x ( z ( +g ` O ) y ) e. x ) ) )
21 4 20 sylbi 
 |-  ( G e. Mnd -> ( x e. ( SubMnd ` O ) <-> ( x C_ ( Base ` G ) /\ ( 0g ` G ) e. x /\ A. z e. x A. y e. x ( z ( +g ` O ) y ) e. x ) ) )
22 14 17 21 3bitr4d 
 |-  ( G e. Mnd -> ( x e. ( SubMnd ` G ) <-> x e. ( SubMnd ` O ) ) )
23 2 5 22 pm5.21nii 
 |-  ( x e. ( SubMnd ` G ) <-> x e. ( SubMnd ` O ) )
24 23 eqriv 
 |-  ( SubMnd ` G ) = ( SubMnd ` O )