Metamath Proof Explorer

Theorem opnsubg

Description: An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015)

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

Proof

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