Metamath Proof Explorer

Theorem oppgtmd

Description: The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypothesis oppgtmd.1 
|- O = ( oppG ` G )
Assertion oppgtmd 
|- ( G e. TopMnd -> O e. TopMnd )

Proof

Step Hyp Ref Expression
1 oppgtmd.1 
 |-  O = ( oppG ` G )
2 tmdmnd 
 |-  ( G e. TopMnd -> G e. Mnd )
3 1 oppgmnd 
 |-  ( G e. Mnd -> O e. Mnd )
4 2 3 syl 
 |-  ( G e. TopMnd -> O e. Mnd )
5 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 5 6 tmdtopon 
 |-  ( G e. TopMnd -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
8 1 6 oppgbas 
 |-  ( Base ` G ) = ( Base ` O )
9 1 5 oppgtopn 
 |-  ( TopOpen ` G ) = ( TopOpen ` O )
10 8 9 istps 
 |-  ( O e. TopSp <-> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
11 7 10 sylibr 
 |-  ( G e. TopMnd -> O e. TopSp )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 id 
 |-  ( G e. TopMnd -> G e. TopMnd )
14 7 7 cnmpt2nd 
 |-  ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> y ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
15 7 7 cnmpt1st 
 |-  ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> x ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
16 5 12 13 7 7 14 15 cnmpt2plusg 
 |-  ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
17 eqid 
 |-  ( +g ` O ) = ( +g ` O )
18 eqid 
 |-  ( +f ` O ) = ( +f ` O )
19 8 17 18 plusffval 
 |-  ( +f ` O ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` O ) y ) )
20 12 1 17 oppgplus 
 |-  ( x ( +g ` O ) y ) = ( y ( +g ` G ) x )
21 6 6 20 mpoeq123i 
 |-  ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` O ) y ) ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) )
22 19 21 eqtr2i 
 |-  ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) = ( +f ` O )
23 22 9 istmd 
 |-  ( O e. TopMnd <-> ( O e. Mnd /\ O e. TopSp /\ ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( y ( +g ` G ) x ) ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) )
24 4 11 16 23 syl3anbrc 
 |-  ( G e. TopMnd -> O e. TopMnd )