Metamath Proof Explorer

Theorem oppggrpb

Description: Bidirectional form of oppggrp . (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypothesis oppgbas.1 
|- O = ( oppG ` R )
Assertion oppggrpb 
|- ( R e. Grp <-> O e. Grp )

Proof

Step Hyp Ref Expression
1 oppgbas.1 
 |-  O = ( oppG ` R )
2 1 oppggrp 
 |-  ( R e. Grp -> O e. Grp )
3 eqid 
 |-  ( oppG ` O ) = ( oppG ` O )
4 3 oppggrp 
 |-  ( O e. Grp -> ( oppG ` O ) e. Grp )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 1 5 oppgbas 
 |-  ( Base ` R ) = ( Base ` O )
7 3 6 oppgbas 
 |-  ( Base ` R ) = ( Base ` ( oppG ` O ) )
8 7 a1i 
 |-  ( T. -> ( Base ` R ) = ( Base ` ( oppG ` O ) ) )
9 eqidd 
 |-  ( T. -> ( Base ` R ) = ( Base ` R ) )
10 eqid 
 |-  ( +g ` O ) = ( +g ` O )
11 eqid 
 |-  ( +g ` ( oppG ` O ) ) = ( +g ` ( oppG ` O ) )
12 10 3 11 oppgplus 
 |-  ( x ( +g ` ( oppG ` O ) ) y ) = ( y ( +g ` O ) x )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 13 1 10 oppgplus 
 |-  ( y ( +g ` O ) x ) = ( x ( +g ` R ) y )
15 12 14 eqtri 
 |-  ( x ( +g ` ( oppG ` O ) ) y ) = ( x ( +g ` R ) y )
16 15 a1i 
 |-  ( ( T. /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` ( oppG ` O ) ) y ) = ( x ( +g ` R ) y ) )
17 8 9 16 grppropd 
 |-  ( T. -> ( ( oppG ` O ) e. Grp <-> R e. Grp ) )
18 17 mptru 
 |-  ( ( oppG ` O ) e. Grp <-> R e. Grp )
19 4 18 sylib 
 |-  ( O e. Grp -> R e. Grp )
20 2 19 impbii 
 |-  ( R e. Grp <-> O e. Grp )