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