Step |
Hyp |
Ref |
Expression |
1 |
|
qustgp.h |
|- H = ( G /s ( G ~QG Y ) ) |
2 |
|
qustgphaus.j |
|- J = ( TopOpen ` G ) |
3 |
|
qustgphaus.k |
|- K = ( TopOpen ` H ) |
4 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
5 |
1 4
|
qus0 |
|- ( Y e. ( NrmSGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG Y ) = ( 0g ` H ) ) |
6 |
5
|
3ad2ant2 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] ( G ~QG Y ) = ( 0g ` H ) ) |
7 |
|
tgpgrp |
|- ( G e. TopGrp -> G e. Grp ) |
8 |
7
|
3ad2ant1 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> G e. Grp ) |
9 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
10 |
9 4
|
grpidcl |
|- ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) ) |
11 |
8 10
|
syl |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( 0g ` G ) e. ( Base ` G ) ) |
12 |
|
ovex |
|- ( G ~QG Y ) e. _V |
13 |
12
|
ecelqsi |
|- ( ( 0g ` G ) e. ( Base ` G ) -> [ ( 0g ` G ) ] ( G ~QG Y ) e. ( ( Base ` G ) /. ( G ~QG Y ) ) ) |
14 |
11 13
|
syl |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] ( G ~QG Y ) e. ( ( Base ` G ) /. ( G ~QG Y ) ) ) |
15 |
6 14
|
eqeltrrd |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( 0g ` H ) e. ( ( Base ` G ) /. ( G ~QG Y ) ) ) |
16 |
15
|
snssd |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> { ( 0g ` H ) } C_ ( ( Base ` G ) /. ( G ~QG Y ) ) ) |
17 |
|
eqid |
|- ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) = ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) |
18 |
17
|
mptpreima |
|- ( `' ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) " { ( 0g ` H ) } ) = { x e. ( Base ` G ) | [ x ] ( G ~QG Y ) e. { ( 0g ` H ) } } |
19 |
|
nsgsubg |
|- ( Y e. ( NrmSGrp ` G ) -> Y e. ( SubGrp ` G ) ) |
20 |
19
|
3ad2ant2 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> Y e. ( SubGrp ` G ) ) |
21 |
|
eqid |
|- ( G ~QG Y ) = ( G ~QG Y ) |
22 |
9 21 4
|
eqgid |
|- ( Y e. ( SubGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG Y ) = Y ) |
23 |
20 22
|
syl |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] ( G ~QG Y ) = Y ) |
24 |
9
|
subgss |
|- ( Y e. ( SubGrp ` G ) -> Y C_ ( Base ` G ) ) |
25 |
20 24
|
syl |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> Y C_ ( Base ` G ) ) |
26 |
23 25
|
eqsstrd |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> [ ( 0g ` G ) ] ( G ~QG Y ) C_ ( Base ` G ) ) |
27 |
|
sseqin2 |
|- ( [ ( 0g ` G ) ] ( G ~QG Y ) C_ ( Base ` G ) <-> ( ( Base ` G ) i^i [ ( 0g ` G ) ] ( G ~QG Y ) ) = [ ( 0g ` G ) ] ( G ~QG Y ) ) |
28 |
26 27
|
sylib |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( ( Base ` G ) i^i [ ( 0g ` G ) ] ( G ~QG Y ) ) = [ ( 0g ` G ) ] ( G ~QG Y ) ) |
29 |
9 21
|
eqger |
|- ( Y e. ( SubGrp ` G ) -> ( G ~QG Y ) Er ( Base ` G ) ) |
30 |
20 29
|
syl |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( G ~QG Y ) Er ( Base ` G ) ) |
31 |
30 11
|
erth |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( ( 0g ` G ) ( G ~QG Y ) x <-> [ ( 0g ` G ) ] ( G ~QG Y ) = [ x ] ( G ~QG Y ) ) ) |
32 |
31
|
adantr |
|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) /\ x e. ( Base ` G ) ) -> ( ( 0g ` G ) ( G ~QG Y ) x <-> [ ( 0g ` G ) ] ( G ~QG Y ) = [ x ] ( G ~QG Y ) ) ) |
33 |
6
|
adantr |
|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) /\ x e. ( Base ` G ) ) -> [ ( 0g ` G ) ] ( G ~QG Y ) = ( 0g ` H ) ) |
34 |
33
|
eqeq1d |
|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) /\ x e. ( Base ` G ) ) -> ( [ ( 0g ` G ) ] ( G ~QG Y ) = [ x ] ( G ~QG Y ) <-> ( 0g ` H ) = [ x ] ( G ~QG Y ) ) ) |
35 |
32 34
|
bitrd |
|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) /\ x e. ( Base ` G ) ) -> ( ( 0g ` G ) ( G ~QG Y ) x <-> ( 0g ` H ) = [ x ] ( G ~QG Y ) ) ) |
36 |
|
vex |
|- x e. _V |
37 |
|
fvex |
|- ( 0g ` G ) e. _V |
38 |
36 37
|
elec |
|- ( x e. [ ( 0g ` G ) ] ( G ~QG Y ) <-> ( 0g ` G ) ( G ~QG Y ) x ) |
39 |
|
fvex |
|- ( 0g ` H ) e. _V |
40 |
39
|
elsn2 |
|- ( [ x ] ( G ~QG Y ) e. { ( 0g ` H ) } <-> [ x ] ( G ~QG Y ) = ( 0g ` H ) ) |
41 |
|
eqcom |
|- ( [ x ] ( G ~QG Y ) = ( 0g ` H ) <-> ( 0g ` H ) = [ x ] ( G ~QG Y ) ) |
42 |
40 41
|
bitri |
|- ( [ x ] ( G ~QG Y ) e. { ( 0g ` H ) } <-> ( 0g ` H ) = [ x ] ( G ~QG Y ) ) |
43 |
35 38 42
|
3bitr4g |
|- ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) /\ x e. ( Base ` G ) ) -> ( x e. [ ( 0g ` G ) ] ( G ~QG Y ) <-> [ x ] ( G ~QG Y ) e. { ( 0g ` H ) } ) ) |
44 |
43
|
rabbi2dva |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( ( Base ` G ) i^i [ ( 0g ` G ) ] ( G ~QG Y ) ) = { x e. ( Base ` G ) | [ x ] ( G ~QG Y ) e. { ( 0g ` H ) } } ) |
45 |
28 44 23
|
3eqtr3d |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> { x e. ( Base ` G ) | [ x ] ( G ~QG Y ) e. { ( 0g ` H ) } } = Y ) |
46 |
18 45
|
eqtrid |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( `' ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) " { ( 0g ` H ) } ) = Y ) |
47 |
|
simp3 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> Y e. ( Clsd ` J ) ) |
48 |
46 47
|
eqeltrd |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( `' ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) " { ( 0g ` H ) } ) e. ( Clsd ` J ) ) |
49 |
2 9
|
tgptopon |
|- ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) ) |
50 |
49
|
3ad2ant1 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> J e. ( TopOn ` ( Base ` G ) ) ) |
51 |
1
|
a1i |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> H = ( G /s ( G ~QG Y ) ) ) |
52 |
|
eqidd |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( Base ` G ) = ( Base ` G ) ) |
53 |
12
|
a1i |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( G ~QG Y ) e. _V ) |
54 |
|
simp1 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> G e. TopGrp ) |
55 |
51 52 17 53 54
|
quslem |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) : ( Base ` G ) -onto-> ( ( Base ` G ) /. ( G ~QG Y ) ) ) |
56 |
|
qtopcld |
|- ( ( J e. ( TopOn ` ( Base ` G ) ) /\ ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) : ( Base ` G ) -onto-> ( ( Base ` G ) /. ( G ~QG Y ) ) ) -> ( { ( 0g ` H ) } e. ( Clsd ` ( J qTop ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) ) ) <-> ( { ( 0g ` H ) } C_ ( ( Base ` G ) /. ( G ~QG Y ) ) /\ ( `' ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) " { ( 0g ` H ) } ) e. ( Clsd ` J ) ) ) ) |
57 |
50 55 56
|
syl2anc |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( { ( 0g ` H ) } e. ( Clsd ` ( J qTop ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) ) ) <-> ( { ( 0g ` H ) } C_ ( ( Base ` G ) /. ( G ~QG Y ) ) /\ ( `' ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) " { ( 0g ` H ) } ) e. ( Clsd ` J ) ) ) ) |
58 |
16 48 57
|
mpbir2and |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> { ( 0g ` H ) } e. ( Clsd ` ( J qTop ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) ) ) ) |
59 |
51 52 17 53 54
|
qusval |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> H = ( ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) "s G ) ) |
60 |
59 52 55 54 2 3
|
imastopn |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> K = ( J qTop ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) ) ) |
61 |
60
|
fveq2d |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( Clsd ` K ) = ( Clsd ` ( J qTop ( x e. ( Base ` G ) |-> [ x ] ( G ~QG Y ) ) ) ) ) |
62 |
58 61
|
eleqtrrd |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> { ( 0g ` H ) } e. ( Clsd ` K ) ) |
63 |
1
|
qustgp |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp ) |
64 |
63
|
3adant3 |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> H e. TopGrp ) |
65 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
66 |
65 3
|
tgphaus |
|- ( H e. TopGrp -> ( K e. Haus <-> { ( 0g ` H ) } e. ( Clsd ` K ) ) ) |
67 |
64 66
|
syl |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> ( K e. Haus <-> { ( 0g ` H ) } e. ( Clsd ` K ) ) ) |
68 |
62 67
|
mpbird |
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> K e. Haus ) |