This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgpcn

Description: In a topological group, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010) (Revised by Mario Carneiro, 13-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 tgpcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgpcn.1 ⊢ 𝐹 = ( +𝑓 ‘ 𝐺 )
3 tgptmd ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
4 1 2 tmdcn ⊢ ( 𝐺 ∈ TopMnd → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
5 3 4 syl ⊢ ( 𝐺 ∈ TopGrp → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )