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 )