Metamath Proof Explorer

Theorem subgntr

Description: A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg , the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 subgntr.h 
 |-  J = ( TopOpen ` G )
2 df-ima 
 |-  ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) " ( ( int ` J ) ` S ) ) = ran ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) |` ( ( int ` J ) ` S ) )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 1 3 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
5 4 3ad2ant1 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> J e. ( TopOn ` ( Base ` G ) ) )
6 5 adantr 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> J e. ( TopOn ` ( Base ` G ) ) )
7 topontop 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> J e. Top )
8 5 7 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> J e. Top )
9 8 adantr 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> J e. Top )
10 simpl2 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> S e. ( SubGrp ` G ) )
11 3 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
12 10 11 syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> S C_ ( Base ` G ) )
13 toponuni 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( Base ` G ) = U. J )
14 6 13 syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( Base ` G ) = U. J )
15 12 14 sseqtrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> S C_ U. J )
16 eqid 
 |-  U. J = U. J
17 16 ntropn 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( int ` J ) ` S ) e. J )
18 9 15 17 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( int ` J ) ` S ) e. J )
19 toponss 
 |-  ( ( J e. ( TopOn ` ( Base ` G ) ) /\ ( ( int ` J ) ` S ) e. J ) -> ( ( int ` J ) ` S ) C_ ( Base ` G ) )
20 6 18 19 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( int ` J ) ` S ) C_ ( Base ` G ) )
21 20 resmptd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) |` ( ( int ` J ) ` S ) ) = ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) )
22 21 rneqd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ran ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) |` ( ( int ` J ) ` S ) ) = ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) )
23 2 22 syl5eq 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) " ( ( int ` J ) ` S ) ) = ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) )
24 simpl1 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> G e. TopGrp )
25 simpr 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> x e. S )
26 16 ntrss2 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( int ` J ) ` S ) C_ S )
27 9 15 26 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( int ` J ) ` S ) C_ S )
28 simpl3 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> A e. ( ( int ` J ) ` S ) )
29 27 28 sseldd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> A e. S )
30 eqid 
 |-  ( -g ` G ) = ( -g ` G )
31 30 subgsubcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S /\ A e. S ) -> ( x ( -g ` G ) A ) e. S )
32 10 25 29 31 syl3anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( x ( -g ` G ) A ) e. S )
33 12 32 sseldd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( x ( -g ` G ) A ) e. ( Base ` G ) )
34 eqid 
 |-  ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) = ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) )
35 eqid 
 |-  ( +g ` G ) = ( +g ` G )
36 34 3 35 1 tgplacthmeo 
 |-  ( ( G e. TopGrp /\ ( x ( -g ` G ) A ) e. ( Base ` G ) ) -> ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) e. ( J Homeo J ) )
37 24 33 36 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) e. ( J Homeo J ) )
38 hmeoima 
 |-  ( ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) e. ( J Homeo J ) /\ ( ( int ` J ) ` S ) e. J ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) " ( ( int ` J ) ` S ) ) e. J )
39 37 18 38 syl2anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( y e. ( Base ` G ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) " ( ( int ` J ) ` S ) ) e. J )
40 23 39 eqeltrrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) e. J )
41 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
42 24 41 syl 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> G e. Grp )
43 11 3ad2ant2 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> S C_ ( Base ` G ) )
44 43 sselda 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> x e. ( Base ` G ) )
45 20 28 sseldd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> A e. ( Base ` G ) )
46 3 35 30 grpnpcan 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) /\ A e. ( Base ` G ) ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) A ) = x )
47 42 44 45 46 syl3anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) A ) = x )
48 ovex 
 |-  ( ( x ( -g ` G ) A ) ( +g ` G ) A ) e. _V
49 eqid 
 |-  ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) = ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) )
50 oveq2 
 |-  ( y = A -> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) = ( ( x ( -g ` G ) A ) ( +g ` G ) A ) )
51 49 50 elrnmpt1s 
 |-  ( ( A e. ( ( int ` J ) ` S ) /\ ( ( x ( -g ` G ) A ) ( +g ` G ) A ) e. _V ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) A ) e. ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) )
52 28 48 51 sylancl 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) A ) e. ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) )
53 47 52 eqeltrrd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> x e. ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) )
54 10 adantr 
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) /\ y e. ( ( int ` J ) ` S ) ) -> S e. ( SubGrp ` G ) )
55 32 adantr 
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) /\ y e. ( ( int ` J ) ` S ) ) -> ( x ( -g ` G ) A ) e. S )
56 27 sselda 
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) /\ y e. ( ( int ` J ) ` S ) ) -> y e. S )
57 35 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( x ( -g ` G ) A ) e. S /\ y e. S ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) e. S )
58 54 55 56 57 syl3anc 
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) /\ y e. ( ( int ` J ) ` S ) ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) e. S )
59 58 fmpttd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) : ( ( int ` J ) ` S ) --> S )
60 59 frnd 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) C_ S )
61 eleq2 
 |-  ( u = ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) -> ( x e. u <-> x e. ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) ) )
62 sseq1 
 |-  ( u = ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) -> ( u C_ S <-> ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) C_ S ) )
63 61 62 anbi12d 
 |-  ( u = ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) -> ( ( x e. u /\ u C_ S ) <-> ( x e. ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) /\ ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) C_ S ) ) )
64 63 rspcev 
 |-  ( ( ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) e. J /\ ( x e. ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) /\ ran ( y e. ( ( int ` J ) ` S ) |-> ( ( x ( -g ` G ) A ) ( +g ` G ) y ) ) C_ S ) ) -> E. u e. J ( x e. u /\ u C_ S ) )
65 40 53 60 64 syl12anc 
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) /\ x e. S ) -> E. u e. J ( x e. u /\ u C_ S ) )
66 65 ralrimiva 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> A. x e. S E. u e. J ( x e. u /\ u C_ S ) )
67 eltop2 
 |-  ( J e. Top -> ( S e. J <-> A. x e. S E. u e. J ( x e. u /\ u C_ S ) ) )
68 8 67 syl 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> ( S e. J <-> A. x e. S E. u e. J ( x e. u /\ u C_ S ) ) )
69 66 68 mpbird 
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> S e. J )