Metamath Proof Explorer


Theorem cldsubg

Description: A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses subgntr.h
|- J = ( TopOpen ` G )
cldsubg.1
|- R = ( G ~QG S )
cldsubg.2
|- X = ( Base ` G )
Assertion cldsubg
|- ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) <-> S e. J ) )

Proof

Step Hyp Ref Expression
1 subgntr.h
 |-  J = ( TopOpen ` G )
2 cldsubg.1
 |-  R = ( G ~QG S )
3 cldsubg.2
 |-  X = ( Base ` G )
4 simpl1
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> G e. TopGrp )
5 1 3 tgptopon
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
6 4 5 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> J e. ( TopOn ` X ) )
7 toponuni
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
8 6 7 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> X = U. J )
9 8 difeq1d
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X \ U. ( ( X /. R ) \ { S } ) ) = ( U. J \ U. ( ( X /. R ) \ { S } ) ) )
10 simpl2
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. ( SubGrp ` G ) )
11 unisng
 |-  ( S e. ( SubGrp ` G ) -> U. { S } = S )
12 10 11 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. { S } = S )
13 12 uneq2d
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. U. { S } ) = ( U. ( ( X /. R ) \ { S } ) u. S ) )
14 uniun
 |-  U. ( ( ( X /. R ) \ { S } ) u. { S } ) = ( U. ( ( X /. R ) \ { S } ) u. U. { S } )
15 undif1
 |-  ( ( ( X /. R ) \ { S } ) u. { S } ) = ( ( X /. R ) u. { S } )
16 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
17 3 2 16 eqgid
 |-  ( S e. ( SubGrp ` G ) -> [ ( 0g ` G ) ] R = S )
18 10 17 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] R = S )
19 2 ovexi
 |-  R e. _V
20 tgpgrp
 |-  ( G e. TopGrp -> G e. Grp )
21 4 20 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> G e. Grp )
22 3 16 grpidcl
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
23 21 22 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( 0g ` G ) e. X )
24 ecelqsg
 |-  ( ( R e. _V /\ ( 0g ` G ) e. X ) -> [ ( 0g ` G ) ] R e. ( X /. R ) )
25 19 23 24 sylancr
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] R e. ( X /. R ) )
26 18 25 eqeltrrd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. ( X /. R ) )
27 26 snssd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> { S } C_ ( X /. R ) )
28 ssequn2
 |-  ( { S } C_ ( X /. R ) <-> ( ( X /. R ) u. { S } ) = ( X /. R ) )
29 27 28 sylib
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) u. { S } ) = ( X /. R ) )
30 15 29 syl5eq
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( ( X /. R ) \ { S } ) u. { S } ) = ( X /. R ) )
31 30 unieqd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( ( X /. R ) \ { S } ) u. { S } ) = U. ( X /. R ) )
32 3 2 eqger
 |-  ( S e. ( SubGrp ` G ) -> R Er X )
33 10 32 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> R Er X )
34 19 a1i
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> R e. _V )
35 33 34 uniqs2
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( X /. R ) = X )
36 31 35 eqtrd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( ( X /. R ) \ { S } ) u. { S } ) = X )
37 14 36 eqtr3id
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. U. { S } ) = X )
38 13 37 eqtr3d
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) u. S ) = X )
39 difss
 |-  ( ( X /. R ) \ { S } ) C_ ( X /. R )
40 39 unissi
 |-  U. ( ( X /. R ) \ { S } ) C_ U. ( X /. R )
41 40 35 sseqtrid
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) C_ X )
42 df-ne
 |-  ( x =/= S <-> -. x = S )
43 33 adantr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> R Er X )
44 simpr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> x e. ( X /. R ) )
45 26 adantr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> S e. ( X /. R ) )
46 43 44 45 qsdisj
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( x = S \/ ( x i^i S ) = (/) ) )
47 46 ord
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( -. x = S -> ( x i^i S ) = (/) ) )
48 disj2
 |-  ( ( x i^i S ) = (/) <-> x C_ ( _V \ S ) )
49 47 48 syl6ib
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( -. x = S -> x C_ ( _V \ S ) ) )
50 42 49 syl5bi
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ x e. ( X /. R ) ) -> ( x =/= S -> x C_ ( _V \ S ) ) )
51 50 expimpd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( x e. ( X /. R ) /\ x =/= S ) -> x C_ ( _V \ S ) ) )
52 eldifsn
 |-  ( x e. ( ( X /. R ) \ { S } ) <-> ( x e. ( X /. R ) /\ x =/= S ) )
53 velpw
 |-  ( x e. ~P ( _V \ S ) <-> x C_ ( _V \ S ) )
54 51 52 53 3imtr4g
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( x e. ( ( X /. R ) \ { S } ) -> x e. ~P ( _V \ S ) ) )
55 54 ssrdv
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) C_ ~P ( _V \ S ) )
56 sspwuni
 |-  ( ( ( X /. R ) \ { S } ) C_ ~P ( _V \ S ) <-> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
57 55 56 sylib
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
58 disj2
 |-  ( ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) <-> U. ( ( X /. R ) \ { S } ) C_ ( _V \ S ) )
59 57 58 sylibr
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) )
60 uneqdifeq
 |-  ( ( U. ( ( X /. R ) \ { S } ) C_ X /\ ( U. ( ( X /. R ) \ { S } ) i^i S ) = (/) ) -> ( ( U. ( ( X /. R ) \ { S } ) u. S ) = X <-> ( X \ U. ( ( X /. R ) \ { S } ) ) = S ) )
61 41 59 60 syl2anc
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( U. ( ( X /. R ) \ { S } ) u. S ) = X <-> ( X \ U. ( ( X /. R ) \ { S } ) ) = S ) )
62 38 61 mpbid
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X \ U. ( ( X /. R ) \ { S } ) ) = S )
63 9 62 eqtr3d
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) = S )
64 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
65 6 64 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> J e. Top )
66 simpl3
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) e. Fin )
67 diffi
 |-  ( ( X /. R ) e. Fin -> ( ( X /. R ) \ { S } ) e. Fin )
68 66 67 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) e. Fin )
69 vex
 |-  x e. _V
70 69 elqs
 |-  ( x e. ( X /. R ) <-> E. y e. X x = [ y ] R )
71 simpll2
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S e. ( SubGrp ` G ) )
72 subgrcl
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
73 71 72 syl
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> G e. Grp )
74 3 subgss
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
75 10 74 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S C_ X )
76 75 adantr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S C_ X )
77 simpr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> y e. X )
78 eqid
 |-  ( +g ` G ) = ( +g ` G )
79 3 2 78 eqglact
 |-  ( ( G e. Grp /\ S C_ X /\ y e. X ) -> [ y ] R = ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) )
80 73 76 77 79 syl3anc
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> [ y ] R = ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) )
81 simplr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S e. ( Clsd ` J ) )
82 eqid
 |-  ( z e. X |-> ( y ( +g ` G ) z ) ) = ( z e. X |-> ( y ( +g ` G ) z ) )
83 82 3 78 1 tgplacthmeo
 |-  ( ( G e. TopGrp /\ y e. X ) -> ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) )
84 4 83 sylan
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) )
85 75 8 sseqtrd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S C_ U. J )
86 85 adantr
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> S C_ U. J )
87 eqid
 |-  U. J = U. J
88 87 hmeocld
 |-  ( ( ( z e. X |-> ( y ( +g ` G ) z ) ) e. ( J Homeo J ) /\ S C_ U. J ) -> ( S e. ( Clsd ` J ) <-> ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) e. ( Clsd ` J ) ) )
89 84 86 88 syl2anc
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( S e. ( Clsd ` J ) <-> ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) e. ( Clsd ` J ) ) )
90 81 89 mpbid
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( ( z e. X |-> ( y ( +g ` G ) z ) ) " S ) e. ( Clsd ` J ) )
91 80 90 eqeltrd
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> [ y ] R e. ( Clsd ` J ) )
92 eleq1
 |-  ( x = [ y ] R -> ( x e. ( Clsd ` J ) <-> [ y ] R e. ( Clsd ` J ) ) )
93 91 92 syl5ibrcom
 |-  ( ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) /\ y e. X ) -> ( x = [ y ] R -> x e. ( Clsd ` J ) ) )
94 93 rexlimdva
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( E. y e. X x = [ y ] R -> x e. ( Clsd ` J ) ) )
95 70 94 syl5bi
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( x e. ( X /. R ) -> x e. ( Clsd ` J ) ) )
96 95 ssrdv
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( X /. R ) C_ ( Clsd ` J ) )
97 96 ssdifssd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) )
98 87 unicld
 |-  ( ( J e. Top /\ ( ( X /. R ) \ { S } ) e. Fin /\ ( ( X /. R ) \ { S } ) C_ ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
99 65 68 97 98 syl3anc
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) )
100 87 cldopn
 |-  ( U. ( ( X /. R ) \ { S } ) e. ( Clsd ` J ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) e. J )
101 99 100 syl
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> ( U. J \ U. ( ( X /. R ) \ { S } ) ) e. J )
102 63 101 eqeltrrd
 |-  ( ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) /\ S e. ( Clsd ` J ) ) -> S e. J )
103 102 ex
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) -> S e. J ) )
104 1 opnsubg
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ S e. J ) -> S e. ( Clsd ` J ) )
105 104 3expia
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
106 105 3adant3
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. J -> S e. ( Clsd ` J ) ) )
107 103 106 impbid
 |-  ( ( G e. TopGrp /\ S e. ( SubGrp ` G ) /\ ( X /. R ) e. Fin ) -> ( S e. ( Clsd ` J ) <-> S e. J ) )