Metamath Proof Explorer

Theorem clssubg

Description: The closure of a subgroup in a topological group is a subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis subgntr.h 
|- J = ( TopOpen ` G )
Assertion clssubg 
|- ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 subgntr.h 
 |-  J = ( TopOpen ` G )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 1 2 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
4 3 adantr 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> J e. ( TopOn ` ( Base ` G ) ) )
5 topontop 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> J e. Top )
6 4 5 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> J e. Top )
7 2 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
8 7 adantl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> S C_ ( Base ` G ) )
9 toponuni 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( Base ` G ) = U. J )
10 4 9 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( Base ` G ) = U. J )
11 8 10 sseqtrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> S C_ U. J )
12 eqid 
 |-  U. J = U. J
13 12 clsss3 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
14 6 11 13 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` J ) ` S ) C_ U. J )
15 14 10 sseqtrrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` J ) ` S ) C_ ( Base ` G ) )
16 12 sscls 
 |-  ( ( J e. Top /\ S C_ U. J ) -> S C_ ( ( cls ` J ) ` S ) )
17 6 11 16 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> S C_ ( ( cls ` J ) ` S ) )
18 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
19 18 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
20 19 adantl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( 0g ` G ) e. S )
21 20 ne0d 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> S =/= (/) )
22 ssn0 
 |-  ( ( S C_ ( ( cls ` J ) ` S ) /\ S =/= (/) ) -> ( ( cls ` J ) ` S ) =/= (/) )
23 17 21 22 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` J ) ` S ) =/= (/) )
24 df-ov 
 |-  ( x ( -g ` G ) y ) = ( ( -g ` G ) ` <. x , y >. )
25 opelxpi 
 |-  ( ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) -> <. x , y >. e. ( ( ( cls ` J ) ` S ) X. ( ( cls ` J ) ` S ) ) )
26 txcls 
 |-  ( ( ( J e. ( TopOn ` ( Base ` G ) ) /\ J e. ( TopOn ` ( Base ` G ) ) ) /\ ( S C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) ) -> ( ( cls ` ( J tX J ) ) ` ( S X. S ) ) = ( ( ( cls ` J ) ` S ) X. ( ( cls ` J ) ` S ) ) )
27 4 4 8 8 26 syl22anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` ( J tX J ) ) ` ( S X. S ) ) = ( ( ( cls ` J ) ` S ) X. ( ( cls ` J ) ` S ) ) )
28 txtopon 
 |-  ( ( J e. ( TopOn ` ( Base ` G ) ) /\ J e. ( TopOn ` ( Base ` G ) ) ) -> ( J tX J ) e. ( TopOn ` ( ( Base ` G ) X. ( Base ` G ) ) ) )
29 4 4 28 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( J tX J ) e. ( TopOn ` ( ( Base ` G ) X. ( Base ` G ) ) ) )
30 topontop 
 |-  ( ( J tX J ) e. ( TopOn ` ( ( Base ` G ) X. ( Base ` G ) ) ) -> ( J tX J ) e. Top )
31 29 30 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( J tX J ) e. Top )
32 cnvimass 
 |-  ( `' ( -g ` G ) " S ) C_ dom ( -g ` G )
33 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
34 33 adantr 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> G e. Grp )
35 eqid 
 |-  ( -g ` G ) = ( -g ` G )
36 2 35 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) )
37 34 36 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) )
38 32 37 fssdm 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( `' ( -g ` G ) " S ) C_ ( ( Base ` G ) X. ( Base ` G ) ) )
39 toponuni 
 |-  ( ( J tX J ) e. ( TopOn ` ( ( Base ` G ) X. ( Base ` G ) ) ) -> ( ( Base ` G ) X. ( Base ` G ) ) = U. ( J tX J ) )
40 29 39 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( Base ` G ) X. ( Base ` G ) ) = U. ( J tX J ) )
41 38 40 sseqtrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( `' ( -g ` G ) " S ) C_ U. ( J tX J ) )
42 35 subgsubcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S /\ y e. S ) -> ( x ( -g ` G ) y ) e. S )
43 42 3expb 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( x e. S /\ y e. S ) ) -> ( x ( -g ` G ) y ) e. S )
44 43 ralrimivva 
 |-  ( S e. ( SubGrp ` G ) -> A. x e. S A. y e. S ( x ( -g ` G ) y ) e. S )
45 fveq2 
 |-  ( z = <. x , y >. -> ( ( -g ` G ) ` z ) = ( ( -g ` G ) ` <. x , y >. ) )
46 45 24 eqtr4di 
 |-  ( z = <. x , y >. -> ( ( -g ` G ) ` z ) = ( x ( -g ` G ) y ) )
47 46 eleq1d 
 |-  ( z = <. x , y >. -> ( ( ( -g ` G ) ` z ) e. S <-> ( x ( -g ` G ) y ) e. S ) )
48 47 ralxp 
 |-  ( A. z e. ( S X. S ) ( ( -g ` G ) ` z ) e. S <-> A. x e. S A. y e. S ( x ( -g ` G ) y ) e. S )
49 44 48 sylibr 
 |-  ( S e. ( SubGrp ` G ) -> A. z e. ( S X. S ) ( ( -g ` G ) ` z ) e. S )
50 49 adantl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> A. z e. ( S X. S ) ( ( -g ` G ) ` z ) e. S )
51 37 ffund 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> Fun ( -g ` G ) )
52 xpss12 
 |-  ( ( S C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( S X. S ) C_ ( ( Base ` G ) X. ( Base ` G ) ) )
53 8 8 52 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( S X. S ) C_ ( ( Base ` G ) X. ( Base ` G ) ) )
54 37 fdmd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> dom ( -g ` G ) = ( ( Base ` G ) X. ( Base ` G ) ) )
55 53 54 sseqtrrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( S X. S ) C_ dom ( -g ` G ) )
56 funimass5 
 |-  ( ( Fun ( -g ` G ) /\ ( S X. S ) C_ dom ( -g ` G ) ) -> ( ( S X. S ) C_ ( `' ( -g ` G ) " S ) <-> A. z e. ( S X. S ) ( ( -g ` G ) ` z ) e. S ) )
57 51 55 56 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( S X. S ) C_ ( `' ( -g ` G ) " S ) <-> A. z e. ( S X. S ) ( ( -g ` G ) ` z ) e. S ) )
58 50 57 mpbird 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( S X. S ) C_ ( `' ( -g ` G ) " S ) )
59 eqid 
 |-  U. ( J tX J ) = U. ( J tX J )
60 59 clsss 
 |-  ( ( ( J tX J ) e. Top /\ ( `' ( -g ` G ) " S ) C_ U. ( J tX J ) /\ ( S X. S ) C_ ( `' ( -g ` G ) " S ) ) -> ( ( cls ` ( J tX J ) ) ` ( S X. S ) ) C_ ( ( cls ` ( J tX J ) ) ` ( `' ( -g ` G ) " S ) ) )
61 31 41 58 60 syl3anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` ( J tX J ) ) ` ( S X. S ) ) C_ ( ( cls ` ( J tX J ) ) ` ( `' ( -g ` G ) " S ) ) )
62 1 35 tgpsubcn 
 |-  ( G e. TopGrp -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
63 62 adantr 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
64 12 cncls2i 
 |-  ( ( ( -g ` G ) e. ( ( J tX J ) Cn J ) /\ S C_ U. J ) -> ( ( cls ` ( J tX J ) ) ` ( `' ( -g ` G ) " S ) ) C_ ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) )
65 63 11 64 syl2anc 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` ( J tX J ) ) ` ( `' ( -g ` G ) " S ) ) C_ ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) )
66 61 65 sstrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` ( J tX J ) ) ` ( S X. S ) ) C_ ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) )
67 27 66 eqsstrrd 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( ( cls ` J ) ` S ) X. ( ( cls ` J ) ` S ) ) C_ ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) )
68 67 sselda 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ <. x , y >. e. ( ( ( cls ` J ) ` S ) X. ( ( cls ` J ) ` S ) ) ) -> <. x , y >. e. ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) )
69 25 68 sylan2 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) ) -> <. x , y >. e. ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) )
70 33 ad2antrr 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) ) -> G e. Grp )
71 ffn 
 |-  ( ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) -> ( -g ` G ) Fn ( ( Base ` G ) X. ( Base ` G ) ) )
72 elpreima 
 |-  ( ( -g ` G ) Fn ( ( Base ` G ) X. ( Base ` G ) ) -> ( <. x , y >. e. ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) <-> ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. ( ( cls ` J ) ` S ) ) ) )
73 70 36 71 72 4syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) ) -> ( <. x , y >. e. ( `' ( -g ` G ) " ( ( cls ` J ) ` S ) ) <-> ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. ( ( cls ` J ) ` S ) ) ) )
74 69 73 mpbid 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) ) -> ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. ( ( cls ` J ) ` S ) ) )
75 74 simprd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) ) -> ( ( -g ` G ) ` <. x , y >. ) e. ( ( cls ` J ) ` S ) )
76 24 75 eqeltrid 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) /\ ( x e. ( ( cls ` J ) ` S ) /\ y e. ( ( cls ` J ) ` S ) ) ) -> ( x ( -g ` G ) y ) e. ( ( cls ` J ) ` S ) )
77 76 ralrimivva 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> A. x e. ( ( cls ` J ) ` S ) A. y e. ( ( cls ` J ) ` S ) ( x ( -g ` G ) y ) e. ( ( cls ` J ) ` S ) )
78 2 35 issubg4 
 |-  ( G e. Grp -> ( ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) <-> ( ( ( cls ` J ) ` S ) C_ ( Base ` G ) /\ ( ( cls ` J ) ` S ) =/= (/) /\ A. x e. ( ( cls ` J ) ` S ) A. y e. ( ( cls ` J ) ` S ) ( x ( -g ` G ) y ) e. ( ( cls ` J ) ` S ) ) ) )
79 34 78 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) <-> ( ( ( cls ` J ) ` S ) C_ ( Base ` G ) /\ ( ( cls ` J ) ` S ) =/= (/) /\ A. x e. ( ( cls ` J ) ` S ) A. y e. ( ( cls ` J ) ` S ) ( x ( -g ` G ) y ) e. ( ( cls ` J ) ` S ) ) ) )
80 15 23 77 79 mpbir3and 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( ( cls ` J ) ` S ) e. ( SubGrp ` G ) )