Metamath Proof Explorer

Theorem tgpconncompeqg

Description: The connected component containing A is the left coset of the identity component containing A . (Contributed by Mario Carneiro, 17-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 tgpconncomp.x 
 |-  X = ( Base ` G )
2 tgpconncomp.z 
 |-  .0. = ( 0g ` G )
3 tgpconncomp.j 
 |-  J = ( TopOpen ` G )
4 tgpconncomp.s 
 |-  S = U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) }
5 tgpconncompeqg.r 
 |-  .~ = ( G ~QG S )
6 dfec2 
 |-  ( A e. X -> [ A ] .~ = { z | A .~ z } )
7 6 adantl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = { z | A .~ z } )
8 ssrab2 
 |-  { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ ~P X
9 sspwuni 
 |-  ( { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ ~P X <-> U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ X )
10 8 9 mpbi 
 |-  U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) } C_ X
11 4 10 eqsstri 
 |-  S C_ X
12 11 a1i 
 |-  ( ( G e. TopGrp /\ A e. X ) -> S C_ X )
13 eqid 
 |-  ( invg ` G ) = ( invg ` G )
14 eqid 
 |-  ( +g ` G ) = ( +g ` G )
15 1 13 14 5 eqgval 
 |-  ( ( G e. TopGrp /\ S C_ X ) -> ( A .~ z <-> ( A e. X /\ z e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) z ) e. S ) ) )
16 12 15 syldan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( A .~ z <-> ( A e. X /\ z e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) z ) e. S ) ) )
17 simp2 
 |-  ( ( A e. X /\ z e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) z ) e. S ) -> z e. X )
18 16 17 syl6bi 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( A .~ z -> z e. X ) )
19 18 abssdv 
 |-  ( ( G e. TopGrp /\ A e. X ) -> { z | A .~ z } C_ X )
20 7 19 eqsstrd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ C_ X )
21 simpr 
 |-  ( ( G e. TopGrp /\ A e. X ) -> A e. X )
22 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
23 1 14 2 13 grplinv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) = .0. )
24 22 23 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) = .0. )
25 3 1 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
26 25 adantr 
 |-  ( ( G e. TopGrp /\ A e. X ) -> J e. ( TopOn ` X ) )
27 22 adantr 
 |-  ( ( G e. TopGrp /\ A e. X ) -> G e. Grp )
28 1 2 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
29 27 28 syl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> .0. e. X )
30 4 conncompid 
 |-  ( ( J e. ( TopOn ` X ) /\ .0. e. X ) -> .0. e. S )
31 26 29 30 syl2anc 
 |-  ( ( G e. TopGrp /\ A e. X ) -> .0. e. S )
32 24 31 eqeltrd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) e. S )
33 1 13 14 5 eqgval 
 |-  ( ( G e. TopGrp /\ S C_ X ) -> ( A .~ A <-> ( A e. X /\ A e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) e. S ) ) )
34 12 33 syldan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( A .~ A <-> ( A e. X /\ A e. X /\ ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) e. S ) ) )
35 21 21 32 34 mpbir3and 
 |-  ( ( G e. TopGrp /\ A e. X ) -> A .~ A )
36 elecg 
 |-  ( ( A e. X /\ A e. X ) -> ( A e. [ A ] .~ <-> A .~ A ) )
37 21 21 36 syl2anc 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( A e. [ A ] .~ <-> A .~ A ) )
38 35 37 mpbird 
 |-  ( ( G e. TopGrp /\ A e. X ) -> A e. [ A ] .~ )
39 1 5 14 eqglact 
 |-  ( ( G e. Grp /\ S C_ X /\ A e. X ) -> [ A ] .~ = ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) )
40 11 39 mp3an2 
 |-  ( ( G e. Grp /\ A e. X ) -> [ A ] .~ = ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) )
41 22 40 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) )
42 41 oveq2d 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( J |`t [ A ] .~ ) = ( J |`t ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) ) )
43 eqid 
 |-  U. J = U. J
44 eqid 
 |-  ( z e. X |-> ( A ( +g ` G ) z ) ) = ( z e. X |-> ( A ( +g ` G ) z ) )
45 44 1 14 3 tgplacthmeo 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Homeo J ) )
46 hmeocn 
 |-  ( ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Homeo J ) -> ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Cn J ) )
47 45 46 syl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Cn J ) )
48 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
49 26 48 syl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> X = U. J )
50 11 49 sseqtrid 
 |-  ( ( G e. TopGrp /\ A e. X ) -> S C_ U. J )
51 4 conncompconn 
 |-  ( ( J e. ( TopOn ` X ) /\ .0. e. X ) -> ( J |`t S ) e. Conn )
52 26 29 51 syl2anc 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( J |`t S ) e. Conn )
53 43 47 50 52 connima 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( J |`t ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) ) e. Conn )
54 42 53 eqeltrd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( J |`t [ A ] .~ ) e. Conn )
55 eqid 
 |-  U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
56 55 conncompss 
 |-  ( ( [ A ] .~ C_ X /\ A e. [ A ] .~ /\ ( J |`t [ A ] .~ ) e. Conn ) -> [ A ] .~ C_ U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )
57 20 38 54 56 syl3anc 
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ C_ U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )
58 elpwi 
 |-  ( y e. ~P X -> y C_ X )
59 44 mptpreima 
 |-  ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) = { z e. X | ( A ( +g ` G ) z ) e. y }
60 59 ssrab3 
 |-  ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) C_ X
61 29 adantr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> .0. e. X )
62 1 14 2 grprid 
 |-  ( ( G e. Grp /\ A e. X ) -> ( A ( +g ` G ) .0. ) = A )
63 22 62 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( A ( +g ` G ) .0. ) = A )
64 63 adantr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( A ( +g ` G ) .0. ) = A )
65 simprrl 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> A e. y )
66 64 65 eqeltrd 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( A ( +g ` G ) .0. ) e. y )
67 oveq2 
 |-  ( z = .0. -> ( A ( +g ` G ) z ) = ( A ( +g ` G ) .0. ) )
68 67 eleq1d 
 |-  ( z = .0. -> ( ( A ( +g ` G ) z ) e. y <-> ( A ( +g ` G ) .0. ) e. y ) )
69 68 59 elrab2 
 |-  ( .0. e. ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) <-> ( .0. e. X /\ ( A ( +g ` G ) .0. ) e. y ) )
70 61 66 69 sylanbrc 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> .0. e. ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) )
71 hmeocnvcn 
 |-  ( ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Homeo J ) -> `' ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Cn J ) )
72 45 71 syl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> `' ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Cn J ) )
73 72 adantr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> `' ( z e. X |-> ( A ( +g ` G ) z ) ) e. ( J Cn J ) )
74 simprl 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> y C_ X )
75 49 adantr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> X = U. J )
76 74 75 sseqtrd 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> y C_ U. J )
77 simprrr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( J |`t y ) e. Conn )
78 43 73 76 77 connima 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( J |`t ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) ) e. Conn )
79 4 conncompss 
 |-  ( ( ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) C_ X /\ .0. e. ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) /\ ( J |`t ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) ) e. Conn ) -> ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) C_ S )
80 60 70 78 79 mp3an2i 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) C_ S )
81 eqid 
 |-  ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) = ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) )
82 81 1 14 13 grplactcnv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) : X -1-1-onto-> X /\ `' ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) = ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` ( ( invg ` G ) ` A ) ) ) )
83 22 82 sylan 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) : X -1-1-onto-> X /\ `' ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) = ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` ( ( invg ` G ) ` A ) ) ) )
84 83 simpld 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) : X -1-1-onto-> X )
85 81 1 grplactfval 
 |-  ( A e. X -> ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) = ( z e. X |-> ( A ( +g ` G ) z ) ) )
86 85 adantl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) = ( z e. X |-> ( A ( +g ` G ) z ) ) )
87 f1oeq1 
 |-  ( ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) = ( z e. X |-> ( A ( +g ` G ) z ) ) -> ( ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) : X -1-1-onto-> X <-> ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X ) )
88 86 87 syl 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( ( ( g e. X |-> ( z e. X |-> ( g ( +g ` G ) z ) ) ) ` A ) : X -1-1-onto-> X <-> ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X ) )
89 84 88 mpbid 
 |-  ( ( G e. TopGrp /\ A e. X ) -> ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X )
90 89 adantr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X )
91 f1ocnv 
 |-  ( ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X -> `' ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X )
92 f1ofun 
 |-  ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X -> Fun `' ( z e. X |-> ( A ( +g ` G ) z ) ) )
93 90 91 92 3syl 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> Fun `' ( z e. X |-> ( A ( +g ` G ) z ) ) )
94 f1odm 
 |-  ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) : X -1-1-onto-> X -> dom `' ( z e. X |-> ( A ( +g ` G ) z ) ) = X )
95 90 91 94 3syl 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> dom `' ( z e. X |-> ( A ( +g ` G ) z ) ) = X )
96 74 95 sseqtrrd 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> y C_ dom `' ( z e. X |-> ( A ( +g ` G ) z ) ) )
97 funimass3 
 |-  ( ( Fun `' ( z e. X |-> ( A ( +g ` G ) z ) ) /\ y C_ dom `' ( z e. X |-> ( A ( +g ` G ) z ) ) ) -> ( ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) C_ S <-> y C_ ( `' `' ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) ) )
98 93 96 97 syl2anc 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> ( ( `' ( z e. X |-> ( A ( +g ` G ) z ) ) " y ) C_ S <-> y C_ ( `' `' ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) ) )
99 80 98 mpbid 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> y C_ ( `' `' ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) )
100 41 adantr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> [ A ] .~ = ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) )
101 imacnvcnv 
 |-  ( `' `' ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) = ( ( z e. X |-> ( A ( +g ` G ) z ) ) " S )
102 100 101 eqtr4di 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> [ A ] .~ = ( `' `' ( z e. X |-> ( A ( +g ` G ) z ) ) " S ) )
103 99 102 sseqtrrd 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ ( y C_ X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) -> y C_ [ A ] .~ )
104 103 expr 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ y C_ X ) -> ( ( A e. y /\ ( J |`t y ) e. Conn ) -> y C_ [ A ] .~ ) )
105 58 104 sylan2 
 |-  ( ( ( G e. TopGrp /\ A e. X ) /\ y e. ~P X ) -> ( ( A e. y /\ ( J |`t y ) e. Conn ) -> y C_ [ A ] .~ ) )
106 105 ralrimiva 
 |-  ( ( G e. TopGrp /\ A e. X ) -> A. y e. ~P X ( ( A e. y /\ ( J |`t y ) e. Conn ) -> y C_ [ A ] .~ ) )
107 eleq2w 
 |-  ( x = y -> ( A e. x <-> A e. y ) )
108 oveq2 
 |-  ( x = y -> ( J |`t x ) = ( J |`t y ) )
109 108 eleq1d 
 |-  ( x = y -> ( ( J |`t x ) e. Conn <-> ( J |`t y ) e. Conn ) )
110 107 109 anbi12d 
 |-  ( x = y -> ( ( A e. x /\ ( J |`t x ) e. Conn ) <-> ( A e. y /\ ( J |`t y ) e. Conn ) ) )
111 110 ralrab 
 |-  ( A. y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y C_ [ A ] .~ <-> A. y e. ~P X ( ( A e. y /\ ( J |`t y ) e. Conn ) -> y C_ [ A ] .~ ) )
112 106 111 sylibr 
 |-  ( ( G e. TopGrp /\ A e. X ) -> A. y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y C_ [ A ] .~ )
113 unissb 
 |-  ( U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } C_ [ A ] .~ <-> A. y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y C_ [ A ] .~ )
114 112 113 sylibr 
 |-  ( ( G e. TopGrp /\ A e. X ) -> U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } C_ [ A ] .~ )
115 57 114 eqssd 
 |-  ( ( G e. TopGrp /\ A e. X ) -> [ A ] .~ = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )