Theorem tmdlactcn

Description: The left group action of element A in a topological monoid G is a continuous function. (Contributed by FL, 18-Mar-2008) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	tgplacthmeo.1	|- F = ( x e. X |-> ( A .+ x ) )
	tgplacthmeo.2	|- X = ( Base ` G )
	tgplacthmeo.3	|- .+ = ( +g ` G )
	tgplacthmeo.4	|- J = ( TopOpen ` G )
Assertion	tmdlactcn	|- ( ( G e. TopMnd /\ A e. X ) -> F e. ( J Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		tgplacthmeo.1	|- F = ( x e. X |-> ( A .+ x ) )
2		tgplacthmeo.2	|- X = ( Base ` G )
3		tgplacthmeo.3	|- .+ = ( +g ` G )
4		tgplacthmeo.4	|- J = ( TopOpen ` G )
5		simpl	|- ( ( G e. TopMnd /\ A e. X ) -> G e. TopMnd )
6	4 2	tmdtopon	|- ( G e. TopMnd -> J e. ( TopOn ` X ) )
7	6	adantr	|- ( ( G e. TopMnd /\ A e. X ) -> J e. ( TopOn ` X ) )
8		simpr	|- ( ( G e. TopMnd /\ A e. X ) -> A e. X )
9	7 7 8	cnmptc	|- ( ( G e. TopMnd /\ A e. X ) -> ( x e. X |-> A ) e. ( J Cn J ) )
10	7	cnmptid	|- ( ( G e. TopMnd /\ A e. X ) -> ( x e. X |-> x ) e. ( J Cn J ) )
11	4 3 5 7 9 10	cnmpt1plusg	|- ( ( G e. TopMnd /\ A e. X ) -> ( x e. X |-> ( A .+ x ) ) e. ( J Cn J ) )
12	1 11	eqeltrid	|- ( ( G e. TopMnd /\ A e. X ) -> F e. ( J Cn J ) )