Metamath Proof Explorer

Theorem oppgmnd

Description: The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 oppgbas.1 
 |-  O = ( oppG ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 1 2 oppgbas 
 |-  ( Base ` R ) = ( Base ` O )
4 3 a1i 
 |-  ( R e. Mnd -> ( Base ` R ) = ( Base ` O ) )
5 eqidd 
 |-  ( R e. Mnd -> ( +g ` O ) = ( +g ` O ) )
6 eqid 
 |-  ( +g ` R ) = ( +g ` R )
7 eqid 
 |-  ( +g ` O ) = ( +g ` O )
8 6 1 7 oppgplus 
 |-  ( x ( +g ` O ) y ) = ( y ( +g ` R ) x )
9 2 6 mndcl 
 |-  ( ( R e. Mnd /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( y ( +g ` R ) x ) e. ( Base ` R ) )
10 9 3com23 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( y ( +g ` R ) x ) e. ( Base ` R ) )
11 8 10 eqeltrid 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` O ) y ) e. ( Base ` R ) )
12 simpl 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> R e. Mnd )
13 simpr3 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> z e. ( Base ` R ) )
14 simpr2 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> y e. ( Base ` R ) )
15 simpr1 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> x e. ( Base ` R ) )
16 2 6 mndass 
 |-  ( ( R e. Mnd /\ ( z e. ( Base ` R ) /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) ) -> ( ( z ( +g ` R ) y ) ( +g ` R ) x ) = ( z ( +g ` R ) ( y ( +g ` R ) x ) ) )
17 12 13 14 15 16 syl13anc 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( z ( +g ` R ) y ) ( +g ` R ) x ) = ( z ( +g ` R ) ( y ( +g ` R ) x ) ) )
18 17 eqcomd 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( z ( +g ` R ) ( y ( +g ` R ) x ) ) = ( ( z ( +g ` R ) y ) ( +g ` R ) x ) )
19 8 oveq1i 
 |-  ( ( x ( +g ` O ) y ) ( +g ` O ) z ) = ( ( y ( +g ` R ) x ) ( +g ` O ) z )
20 6 1 7 oppgplus 
 |-  ( ( y ( +g ` R ) x ) ( +g ` O ) z ) = ( z ( +g ` R ) ( y ( +g ` R ) x ) )
21 19 20 eqtri 
 |-  ( ( x ( +g ` O ) y ) ( +g ` O ) z ) = ( z ( +g ` R ) ( y ( +g ` R ) x ) )
22 6 1 7 oppgplus 
 |-  ( y ( +g ` O ) z ) = ( z ( +g ` R ) y )
23 22 oveq2i 
 |-  ( x ( +g ` O ) ( y ( +g ` O ) z ) ) = ( x ( +g ` O ) ( z ( +g ` R ) y ) )
24 6 1 7 oppgplus 
 |-  ( x ( +g ` O ) ( z ( +g ` R ) y ) ) = ( ( z ( +g ` R ) y ) ( +g ` R ) x )
25 23 24 eqtri 
 |-  ( x ( +g ` O ) ( y ( +g ` O ) z ) ) = ( ( z ( +g ` R ) y ) ( +g ` R ) x )
26 18 21 25 3eqtr4g 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( +g ` O ) y ) ( +g ` O ) z ) = ( x ( +g ` O ) ( y ( +g ` O ) z ) ) )
27 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
28 2 27 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
29 6 1 7 oppgplus 
 |-  ( ( 0g ` R ) ( +g ` O ) x ) = ( x ( +g ` R ) ( 0g ` R ) )
30 2 6 27 mndrid 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) ) -> ( x ( +g ` R ) ( 0g ` R ) ) = x )
31 29 30 syl5eq 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` O ) x ) = x )
32 6 1 7 oppgplus 
 |-  ( x ( +g ` O ) ( 0g ` R ) ) = ( ( 0g ` R ) ( +g ` R ) x )
33 2 6 27 mndlid 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) x ) = x )
34 32 33 syl5eq 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) ) -> ( x ( +g ` O ) ( 0g ` R ) ) = x )
35 4 5 11 26 28 31 34 ismndd 
 |-  ( R e. Mnd -> O e. Mnd )