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 ⊢ 𝑂 = ( oppg ‘ 𝐺 )
Assertion oppgtmd ( 𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 oppgtmd.1 ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 tmdmnd ⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ Mnd )
3 1 oppgmnd ⊢ ( 𝐺 ∈ Mnd → 𝑂 ∈ Mnd )
4 2 3 syl ⊢ ( 𝐺 ∈ TopMnd → 𝑂 ∈ Mnd )
5 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
6 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 5 6 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
8 1 6 oppgbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑂 )
9 1 5 oppgtopn ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝑂 )
10 8 9 istps ⊢ ( 𝑂 ∈ TopSp ↔ ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
11 7 10 sylibr ⊢ ( 𝐺 ∈ TopMnd → 𝑂 ∈ TopSp )
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 id ⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopMnd )
14 7 7 cnmpt2nd ⊢ ( 𝐺 ∈ TopMnd → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑦 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
15 7 7 cnmpt1st ⊢ ( 𝐺 ∈ TopMnd → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
16 5 12 13 7 7 14 15 cnmpt2plusg ⊢ ( 𝐺 ∈ TopMnd → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
17 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
18 eqid ⊢ ( +𝑓 ‘ 𝑂 ) = ( +𝑓 ‘ 𝑂 )
19 8 17 18 plusffval ⊢ ( +𝑓 ‘ 𝑂 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
20 12 1 17 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 )
21 6 6 20 mpoeq123i ⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
22 19 21 eqtr2i ⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( +𝑓 ‘ 𝑂 )
23 22 9 istmd ⊢ ( 𝑂 ∈ TopMnd ↔ ( 𝑂 ∈ Mnd ∧ 𝑂 ∈ TopSp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
24 4 11 16 23 syl3anbrc ⊢ ( 𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd )