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 bitrid 
 |-  ( ( 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 } ) )