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 ) )