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=opp𝑔⁡G
Assertion oppgtmd ⊢G∈TopMnd→O∈TopMnd

Proof

Step Hyp Ref Expression
1 oppgtmd.1 ⊢O=opp𝑔⁡G
2 tmdmnd ⊢G∈TopMnd→G∈Mnd
3 1 oppgmnd ⊢G∈Mnd→O∈Mnd
4 2 3 syl ⊢G∈TopMnd→O∈Mnd
5 eqid ⊢TopOpen⁡G=TopOpen⁡G
6 eqid ⊢BaseG=BaseG
7 5 6 tmdtopon ⊢G∈TopMnd→TopOpen⁡G∈TopOn⁡BaseG
8 1 6 oppgbas ⊢BaseG=BaseO
9 1 5 oppgtopn ⊢TopOpen⁡G=TopOpen⁡O
10 8 9 istps ⊢O∈TopSp↔TopOpen⁡G∈TopOn⁡BaseG
11 7 10 sylibr ⊢G∈TopMnd→O∈TopSp
12 eqid ⊢+G=+G
13 id ⊢G∈TopMnd→G∈TopMnd
14 7 7 cnmpt2nd ⊢G∈TopMnd→x∈BaseG,y∈BaseG⟼y∈TopOpen⁡G×tTopOpen⁡GCnTopOpen⁡G
15 7 7 cnmpt1st ⊢G∈TopMnd→x∈BaseG,y∈BaseG⟼x∈TopOpen⁡G×tTopOpen⁡GCnTopOpen⁡G
16 5 12 13 7 7 14 15 cnmpt2plusg ⊢G∈TopMnd→x∈BaseG,y∈BaseG⟼y+Gx∈TopOpen⁡G×tTopOpen⁡GCnTopOpen⁡G
17 eqid ⊢+O=+O
18 eqid ⊢+𝑓⁡O=+𝑓⁡O
19 8 17 18 plusffval ⊢+𝑓⁡O=x∈BaseG,y∈BaseG⟼x+Oy
20 12 1 17 oppgplus ⊢x+Oy=y+Gx
21 6 6 20 mpoeq123i ⊢x∈BaseG,y∈BaseG⟼x+Oy=x∈BaseG,y∈BaseG⟼y+Gx
22 19 21 eqtr2i ⊢x∈BaseG,y∈BaseG⟼y+Gx=+𝑓⁡O
23 22 9 istmd ⊢O∈TopMnd↔O∈Mnd∧O∈TopSp∧x∈BaseG,y∈BaseG⟼y+Gx∈TopOpen⁡G×tTopOpen⁡GCnTopOpen⁡G
24 4 11 16 23 syl3anbrc ⊢G∈TopMnd→O∈TopMnd