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 )