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	$⊢ J = TopOpen (G)$
	tgpcn.1	$⊢ F = +_{𝑓} (G)$
Assertion	tgpcn	$⊢ G \in TopGrp \to F \in ((J \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		tgpcn.j	$⊢ J = TopOpen (G)$
2		tgpcn.1	$⊢ F = +_{𝑓} (G)$
3		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
4	1 2	tmdcn	$⊢ G \in TopMnd \to F \in ((J \times_{t} J) Cn J)$
5	3 4	syl	$⊢ G \in TopGrp \to F \in ((J \times_{t} J) Cn J)$