Metamath Proof Explorer

Theorem oppgid

Description: Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses oppgbas.1 
|- O = ( oppG ` R )
oppgid.2 
|- .0. = ( 0g ` R )
Assertion oppgid 
|- .0. = ( 0g ` O )

Proof

Step Hyp Ref Expression
1 oppgbas.1 
 |-  O = ( oppG ` R )
2 oppgid.2 
 |-  .0. = ( 0g ` R )
3 ancom 
 |-  ( ( ( x ( +g ` R ) y ) = y /\ ( y ( +g ` R ) x ) = y ) <-> ( ( y ( +g ` R ) x ) = y /\ ( x ( +g ` R ) y ) = y ) )
4 eqid 
 |-  ( +g ` R ) = ( +g ` R )
5 eqid 
 |-  ( +g ` O ) = ( +g ` O )
6 4 1 5 oppgplus 
 |-  ( x ( +g ` O ) y ) = ( y ( +g ` R ) x )
7 6 eqeq1i 
 |-  ( ( x ( +g ` O ) y ) = y <-> ( y ( +g ` R ) x ) = y )
8 4 1 5 oppgplus 
 |-  ( y ( +g ` O ) x ) = ( x ( +g ` R ) y )
9 8 eqeq1i 
 |-  ( ( y ( +g ` O ) x ) = y <-> ( x ( +g ` R ) y ) = y )
10 7 9 anbi12i 
 |-  ( ( ( x ( +g ` O ) y ) = y /\ ( y ( +g ` O ) x ) = y ) <-> ( ( y ( +g ` R ) x ) = y /\ ( x ( +g ` R ) y ) = y ) )
11 3 10 bitr4i 
 |-  ( ( ( x ( +g ` R ) y ) = y /\ ( y ( +g ` R ) x ) = y ) <-> ( ( x ( +g ` O ) y ) = y /\ ( y ( +g ` O ) x ) = y ) )
12 11 ralbii 
 |-  ( A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) = y /\ ( y ( +g ` R ) x ) = y ) <-> A. y e. ( Base ` R ) ( ( x ( +g ` O ) y ) = y /\ ( y ( +g ` O ) x ) = y ) )
13 12 anbi2i 
 |-  ( ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) = y /\ ( y ( +g ` R ) x ) = y ) ) <-> ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( +g ` O ) y ) = y /\ ( y ( +g ` O ) x ) = y ) ) )
14 13 iotabii 
 |-  ( iota x ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) = y /\ ( y ( +g ` R ) x ) = y ) ) ) = ( iota x ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( +g ` O ) y ) = y /\ ( y ( +g ` O ) x ) = y ) ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 15 4 2 grpidval 
 |-  .0. = ( iota x ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( +g ` R ) y ) = y /\ ( y ( +g ` R ) x ) = y ) ) )
17 1 15 oppgbas 
 |-  ( Base ` R ) = ( Base ` O )
18 eqid 
 |-  ( 0g ` O ) = ( 0g ` O )
19 17 5 18 grpidval 
 |-  ( 0g ` O ) = ( iota x ( x e. ( Base ` R ) /\ A. y e. ( Base ` R ) ( ( x ( +g ` O ) y ) = y /\ ( y ( +g ` O ) x ) = y ) ) )
20 14 16 19 3eqtr4i 
 |-  .0. = ( 0g ` O )