Metamath Proof Explorer

Theorem qustgphaus

Description: The quotient of a topological group by a closed normal subgroup is a Hausdorff topological group. In particular, the quotient by the closure of the identity is a Hausdorff topological group, isomorphic to both the Kolmogorov quotient and the Hausdorff quotient operations on topological spaces (because T0 and Hausdorff coincide for topological groups). (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses qustgp.h 
|- H = ( G /s ( G ~QG Y ) )
qustgphaus.j 
|- J = ( TopOpen ` G )
qustgphaus.k 
|- K = ( TopOpen ` H )
Assertion qustgphaus 
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ Y e. ( Clsd ` J ) ) -> K e. Haus )

Proof

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