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 ⊢ Base G = Base G
7 5 6 tmdtopon ⊢ G ∈ TopMnd → TopOpen ⁡ G ∈ TopOn ⁡ Base G
8 1 6 oppgbas ⊢ Base G = Base O
9 1 5 oppgtopn ⊢ TopOpen ⁡ G = TopOpen ⁡ O
10 8 9 istps ⊢ O ∈ TopSp ↔ TopOpen ⁡ G ∈ TopOn ⁡ Base G
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 ∈ Base G , y ∈ Base G ⟼ y ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
15 7 7 cnmpt1st ⊢ G ∈ TopMnd → x ∈ Base G , y ∈ Base G ⟼ x ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
16 5 12 13 7 7 14 15 cnmpt2plusg ⊢ G ∈ TopMnd → x ∈ Base G , y ∈ Base G ⟼ y + G x ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
17 eqid ⊢ + O = + O
18 eqid ⊢ + 𝑓 ⁡ O = + 𝑓 ⁡ O
19 8 17 18 plusffval ⊢ + 𝑓 ⁡ O = x ∈ Base G , y ∈ Base G ⟼ x + O y
20 12 1 17 oppgplus ⊢ x + O y = y + G x
21 6 6 20 mpoeq123i ⊢ x ∈ Base G , y ∈ Base G ⟼ x + O y = x ∈ Base G , y ∈ Base G ⟼ y + G x
22 19 21 eqtr2i ⊢ x ∈ Base G , y ∈ Base G ⟼ y + G x = + 𝑓 ⁡ O
23 22 9 istmd ⊢ O ∈ TopMnd ↔ O ∈ Mnd ∧ O ∈ TopSp ∧ x ∈ Base G , y ∈ Base G ⟼ y + G x ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
24 4 11 16 23 syl3anbrc ⊢ G ∈ TopMnd → O ∈ TopMnd