Metamath Proof Explorer

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 \in X ⟼ A \underset{˙}{+} x)$
		tgplacthmeo.2	$⊢ X = {Base}_{G}$
		tgplacthmeo.3	$⊢ \underset{˙}{+} = +_{G}$
		tgplacthmeo.4	$⊢ J = TopOpen (G)$
	Assertion	tmdlactcn	$⊢ (G \in TopMnd \land A \in X) \to F \in (J Cn J)$

Proof

Step	Hyp	Ref	Expression
1		tgplacthmeo.1	$⊢ F = (x \in X ⟼ A \underset{˙}{+} x)$
2		tgplacthmeo.2	$⊢ X = {Base}_{G}$
3		tgplacthmeo.3	$⊢ \underset{˙}{+} = +_{G}$
4		tgplacthmeo.4	$⊢ J = TopOpen (G)$
5		simpl	$⊢ (G \in TopMnd \land A \in X) \to G \in TopMnd$
6	4 2	tmdtopon	$⊢ G \in TopMnd \to J \in TopOn (X)$
7	6	adantr	$⊢ (G \in TopMnd \land A \in X) \to J \in TopOn (X)$
8		simpr	$⊢ (G \in TopMnd \land A \in X) \to A \in X$
9	7 7 8	cnmptc	$⊢ (G \in TopMnd \land A \in X) \to (x \in X ⟼ A) \in (J Cn J)$
10	7	cnmptid	$⊢ (G \in TopMnd \land A \in X) \to (x \in X ⟼ x) \in (J Cn J)$
11	4 3 5 7 9 10	cnmpt1plusg	$⊢ (G \in TopMnd \land A \in X) \to (x \in X ⟼ A \underset{˙}{+} x) \in (J Cn J)$
12	1 11	eqeltrid	$⊢ (G \in TopMnd \land A \in X) \to F \in (J Cn J)$