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 
|- F = ( x e. X |-> ( A .+ x ) )
tgplacthmeo.2 
|- X = ( Base ` G )
tgplacthmeo.3 
|- .+ = ( +g ` G )
tgplacthmeo.4 
|- J = ( TopOpen ` G )
Assertion tgplacthmeo 
|- ( ( G e. TopGrp /\ A e. X ) -> F e. ( J Homeo J ) )

Proof

Step Hyp Ref Expression
1 tgplacthmeo.1 
 |-  F = ( x e. X |-> ( A .+ x ) )
2 tgplacthmeo.2 
 |-  X = ( Base ` G )
3 tgplacthmeo.3 
 |-  .+ = ( +g ` G )
4 tgplacthmeo.4 
 |-  J = ( TopOpen ` G )
5 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
6 1 2 3 4 tmdlactcn 
 |-  ( ( G e. TopMnd /\ A e. X ) -> F e. ( J Cn J ) )
7 5 6 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> F e. ( J Cn J ) )
8 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
9 eqid 
 |-  ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) = ( g e. X |-> ( x e. X |-> ( g .+ x ) ) )
10 eqid 
 |-  ( invg ` G ) = ( invg ` G )
11 9 2 3 10 grplactcnv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) : X -1-1-onto-> X /\ `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) ) )
12 8 11 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) : X -1-1-onto-> X /\ `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) ) )
13 12 simprd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) )
14 9 2 grplactfval 
 |-  ( A e. X -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( x e. X |-> ( A .+ x ) ) )
15 14 adantl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = ( x e. X |-> ( A .+ x ) ) )
16 15 1 eqtr4di 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = F )
17 16 cnveqd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> `' ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` A ) = `' F )
18 2 10 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
19 8 18 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
20 9 2 grplactfval 
 |-  ( ( ( invg ` G ) ` A ) e. X -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
21 19 20 syl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( g e. X |-> ( x e. X |-> ( g .+ x ) ) ) ` ( ( invg ` G ) ` A ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
22 13 17 21 3eqtr3d 
 |-  ( ( G e. TopGrp /\ A e. X ) -> `' F = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) )
23 eqid 
 |-  ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) = ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) )
24 23 2 3 4 tmdlactcn 
 |-  ( ( G e. TopMnd /\ ( ( invg ` G ) ` A ) e. X ) -> ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) e. ( J Cn J ) )
25 5 19 24 syl2an2r 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( x e. X |-> ( ( ( invg ` G ) ` A ) .+ x ) ) e. ( J Cn J ) )
26 22 25 eqeltrd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> `' F e. ( J Cn J ) )
27 ishmeo 
 |-  ( F e. ( J Homeo J ) <-> ( F e. ( J Cn J ) /\ `' F e. ( J Cn J ) ) )
28 7 26 27 sylanbrc 
 |-  ( ( G e. TopGrp /\ A e. X ) -> F e. ( J Homeo J ) )