This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐽 ) )