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 )