Metamath Proof Explorer


Theorem snclseqg

Description: The coset of the closure of the identity is the closure of a point. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses snclseqg.x
|- X = ( Base ` G )
snclseqg.j
|- J = ( TopOpen ` G )
snclseqg.z
|- .0. = ( 0g ` G )
snclseqg.r
|- .~ = ( G ~QG S )
snclseqg.s
|- S = ( ( cls ` J ) ` { .0. } )
Assertion snclseqg
|- ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( cls ` J ) ` { A } ) )

Proof

Step Hyp Ref Expression
1 snclseqg.x
 |-  X = ( Base ` G )
2 snclseqg.j
 |-  J = ( TopOpen ` G )
3 snclseqg.z
 |-  .0. = ( 0g ` G )
4 snclseqg.r
 |-  .~ = ( G ~QG S )
5 snclseqg.s
 |-  S = ( ( cls ` J ) ` { .0. } )
6 5 imaeq2i
 |-  ( ( x e. X |-> ( A ( +g ` G ) x ) ) " S ) = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " ( ( cls ` J ) ` { .0. } ) )
7 tgpgrp
 |-  ( G e. TopGrp -> G e. Grp )
8 7 adantr
 |-  ( ( G e. TopGrp /\ A e. X ) -> G e. Grp )
9 2 1 tgptopon
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
10 9 adantr
 |-  ( ( G e. TopGrp /\ A e. X ) -> J e. ( TopOn ` X ) )
11 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
12 10 11 syl
 |-  ( ( G e. TopGrp /\ A e. X ) -> J e. Top )
13 1 3 grpidcl
 |-  ( G e. Grp -> .0. e. X )
14 8 13 syl
 |-  ( ( G e. TopGrp /\ A e. X ) -> .0. e. X )
15 14 snssd
 |-  ( ( G e. TopGrp /\ A e. X ) -> { .0. } C_ X )
16 toponuni
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
17 10 16 syl
 |-  ( ( G e. TopGrp /\ A e. X ) -> X = U. J )
18 15 17 sseqtrd
 |-  ( ( G e. TopGrp /\ A e. X ) -> { .0. } C_ U. J )
19 eqid
 |-  U. J = U. J
20 19 clsss3
 |-  ( ( J e. Top /\ { .0. } C_ U. J ) -> ( ( cls ` J ) ` { .0. } ) C_ U. J )
21 12 18 20 syl2anc
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` { .0. } ) C_ U. J )
22 21 17 sseqtrrd
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` { .0. } ) C_ X )
23 5 22 eqsstrid
 |-  ( ( G e. TopGrp /\ A e. X ) -> S C_ X )
24 simpr
 |-  ( ( G e. TopGrp /\ A e. X ) -> A e. X )
25 eqid
 |-  ( +g ` G ) = ( +g ` G )
26 1 4 25 eqglact
 |-  ( ( G e. Grp /\ S C_ X /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " S ) )
27 8 23 24 26 syl3anc
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " S ) )
28 eqid
 |-  ( x e. X |-> ( A ( +g ` G ) x ) ) = ( x e. X |-> ( A ( +g ` G ) x ) )
29 28 1 25 2 tgplacthmeo
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( x e. X |-> ( A ( +g ` G ) x ) ) e. ( J Homeo J ) )
30 19 hmeocls
 |-  ( ( ( x e. X |-> ( A ( +g ` G ) x ) ) e. ( J Homeo J ) /\ { .0. } C_ U. J ) -> ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " ( ( cls ` J ) ` { .0. } ) ) )
31 29 18 30 syl2anc
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) = ( ( x e. X |-> ( A ( +g ` G ) x ) ) " ( ( cls ` J ) ` { .0. } ) ) )
32 6 27 31 3eqtr4a
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) )
33 df-ima
 |-  ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) = ran ( ( x e. X |-> ( A ( +g ` G ) x ) ) |` { .0. } )
34 15 resmptd
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( x e. X |-> ( A ( +g ` G ) x ) ) |` { .0. } ) = ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) )
35 34 rneqd
 |-  ( ( G e. TopGrp /\ A e. X ) -> ran ( ( x e. X |-> ( A ( +g ` G ) x ) ) |` { .0. } ) = ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) )
36 33 35 eqtrid
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) = ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) )
37 3 fvexi
 |-  .0. e. _V
38 oveq2
 |-  ( x = .0. -> ( A ( +g ` G ) x ) = ( A ( +g ` G ) .0. ) )
39 38 eqeq2d
 |-  ( x = .0. -> ( y = ( A ( +g ` G ) x ) <-> y = ( A ( +g ` G ) .0. ) ) )
40 37 39 rexsn
 |-  ( E. x e. { .0. } y = ( A ( +g ` G ) x ) <-> y = ( A ( +g ` G ) .0. ) )
41 1 25 3 grprid
 |-  ( ( G e. Grp /\ A e. X ) -> ( A ( +g ` G ) .0. ) = A )
42 7 41 sylan
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( A ( +g ` G ) .0. ) = A )
43 42 eqeq2d
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( y = ( A ( +g ` G ) .0. ) <-> y = A ) )
44 40 43 syl5bb
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( E. x e. { .0. } y = ( A ( +g ` G ) x ) <-> y = A ) )
45 44 abbidv
 |-  ( ( G e. TopGrp /\ A e. X ) -> { y | E. x e. { .0. } y = ( A ( +g ` G ) x ) } = { y | y = A } )
46 eqid
 |-  ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) = ( x e. { .0. } |-> ( A ( +g ` G ) x ) )
47 46 rnmpt
 |-  ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) = { y | E. x e. { .0. } y = ( A ( +g ` G ) x ) }
48 df-sn
 |-  { A } = { y | y = A }
49 45 47 48 3eqtr4g
 |-  ( ( G e. TopGrp /\ A e. X ) -> ran ( x e. { .0. } |-> ( A ( +g ` G ) x ) ) = { A } )
50 36 49 eqtrd
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) = { A } )
51 50 fveq2d
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( cls ` J ) ` ( ( x e. X |-> ( A ( +g ` G ) x ) ) " { .0. } ) ) = ( ( cls ` J ) ` { A } ) )
52 32 51 eqtrd
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( cls ` J ) ` { A } ) )