Metamath Proof Explorer


Theorem tmdcn

Description: In a topological monoid, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses tgpcn.j 𝐽 = ( TopOpen ‘ 𝐺 )
tgpcn.1 𝐹 = ( +𝑓𝐺 )
Assertion tmdcn ( 𝐺 ∈ TopMnd → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgpcn.1 𝐹 = ( +𝑓𝐺 )
3 2 1 istmd ( 𝐺 ∈ TopMnd ↔ ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
4 3 simp3bi ( 𝐺 ∈ TopMnd → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )