tgplacthmeo

Description: The left group action of element A in a topological group G is a homeomorphism from the group to itself. (Contributed 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	tgplacthmeo	$⊢ (G \in TopGrp \land A \in X) \to F \in (J Homeo 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		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
6	1 2 3 4	tmdlactcn	$⊢ (G \in TopMnd \land A \in X) \to F \in (J Cn J)$
7	5 6	sylan	$⊢ (G \in TopGrp \land A \in X) \to F \in (J Cn J)$
8		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
9		eqid	$⊢ (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x))$
10		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
11	9 2 3 10	grplactcnv	$⊢ (G \in Grp \land A \in X) \to ((g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) : X \underset{1-1 onto}{⟶} X \land {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)))$
12	8 11	sylan	$⊢ (G \in TopGrp \land A \in X) \to ((g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) : X \underset{1-1 onto}{⟶} X \land {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)))$
13	12	simprd	$⊢ (G \in TopGrp \land A \in X) \to {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A))$
14	9 2	grplactfval	$⊢ A \in X \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) = (x \in X ⟼ A \underset{˙}{+} x)$
15	14	adantl	$⊢ (G \in TopGrp \land A \in X) \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) = (x \in X ⟼ A \underset{˙}{+} x)$
16	15 1	eqtr4di	$⊢ (G \in TopGrp \land A \in X) \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A) = F$
17	16	cnveqd	$⊢ (G \in TopGrp \land A \in X) \to {(g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) (A)}^{-1} = F^{-1}$
18	2 10	grpinvcl	$⊢ (G \in Grp \land A \in X) \to {inv}_{g} (G) (A) \in X$
19	8 18	sylan	$⊢ (G \in TopGrp \land A \in X) \to {inv}_{g} (G) (A) \in X$
20	9 2	grplactfval	$⊢ {inv}_{g} (G) (A) \in X \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)) = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
21	19 20	syl	$⊢ (G \in TopGrp \land A \in X) \to (g \in X ⟼ (x \in X ⟼ g \underset{˙}{+} x)) ({inv}_{g} (G) (A)) = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
22	13 17 21	3eqtr3d	$⊢ (G \in TopGrp \land A \in X) \to F^{-1} = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
23		eqid	$⊢ (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x) = (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x)$
24	23 2 3 4	tmdlactcn	$⊢ (G \in TopMnd \land {inv}_{g} (G) (A) \in X) \to (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x) \in (J Cn J)$
25	5 19 24	syl2an2r	$⊢ (G \in TopGrp \land A \in X) \to (x \in X ⟼ {inv}_{g} (G) (A) \underset{˙}{+} x) \in (J Cn J)$
26	22 25	eqeltrd	$⊢ (G \in TopGrp \land A \in X) \to F^{-1} \in (J Cn J)$
27		ishmeo	$⊢ F \in (J Homeo J) \leftrightarrow (F \in (J Cn J) \land F^{-1} \in (J Cn J))$
28	7 26 27	sylanbrc	$⊢ (G \in TopGrp \land A \in X) \to F \in (J Homeo J)$

Metamath Proof Explorer

Theorem tgplacthmeo

Proof