Theorem 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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) )
	tgplacthmeo.2	⊢ 𝑋 = ( Base ‘ 𝐺 )
	tgplacthmeo.3	⊢ + = ( +g ‘ 𝐺 )
	tgplacthmeo.4	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion	tgplacthmeo	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( 𝐽 Homeo 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		tgplacthmeo.1	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) )
2		tgplacthmeo.2	⊢ 𝑋 = ( Base ‘ 𝐺 )
3		tgplacthmeo.3	⊢ + = ( +g ‘ 𝐺 )
4		tgplacthmeo.4	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
5		tgptmd	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
6	1 2 3 4	tmdlactcn	⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
7	5 6	sylan	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
8		tgpgrp	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
9		eqid	⊢ ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) = ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) )
10		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
11	9 2 3 10	grplactcnv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
12	8 11	sylan	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
13	12	simprd	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) )
14	9 2	grplactfval	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) )
15	14	adantl	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝑥 ) ) )
16	15 1	eqtr4di	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = 𝐹 )
17	16	cnveqd	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ 𝐴 ) = ◡ 𝐹 )
18	2 10	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
19	8 18	sylan	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
20	9 2	grplactfval	⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
21	19 20	syl	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 + 𝑥 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
22	13 17 21	3eqtr3d	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ◡ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) )
23		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) )
24	23 2 3 4	tmdlactcn	⊢ ( ( 𝐺 ∈ TopMnd ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
25	5 19 24	syl2an2r	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
26	22 25	eqeltrd	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ◡ 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
27		ishmeo	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐽 ) ↔ ( 𝐹 ∈ ( 𝐽 Cn 𝐽 ) ∧ ◡ 𝐹 ∈ ( 𝐽 Cn 𝐽 ) ) )
28	7 26 27	sylanbrc	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐹 ∈ ( 𝐽 Homeo 𝐽 ) )