This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppgmndb

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

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

Proof

Step Hyp Ref Expression
1 oppgbas.1 
 |-  O = ( oppG ` R )
2 1 oppgmnd 
 |-  ( R e. Mnd -> O e. Mnd )
3 eqid 
 |-  ( oppG ` O ) = ( oppG ` O )
4 3 oppgmnd 
 |-  ( O e. Mnd -> ( oppG ` O ) e. Mnd )
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 mndpropd 
 |-  ( T. -> ( ( oppG ` O ) e. Mnd <-> R e. Mnd ) )
18 17 mptru 
 |-  ( ( oppG ` O ) e. Mnd <-> R e. Mnd )
19 4 18 sylib 
 |-  ( O e. Mnd -> R e. Mnd )
20 2 19 impbii 
 |-  ( R e. Mnd <-> O e. Mnd )