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

Proof

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