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