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 𝐽 ) )