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 ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
qustgphaus.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
qustgphaus.k ⊢ 𝐾 = ( TopOpen ‘ 𝐻 )
Assertion qustgphaus ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐾 ∈ Haus )

Proof

Step Hyp Ref Expression
1 qustgp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
2 qustgphaus.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 qustgphaus.k ⊢ 𝐾 = ( TopOpen ‘ 𝐻 )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 1 4 qus0 ⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = ( 0g ‘ 𝐻 ) )
6 5 3ad2ant2 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = ( 0g ‘ 𝐻 ) )
7 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
8 7 3ad2ant1 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐺 ∈ Grp )
9 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 9 4 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
11 8 10 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
12 ovex ⊢ ( 𝐺 ~QG 𝑌 ) ∈ V
13 12 ecelqsi ⊢ ( ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) )
14 11 13 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) )
15 6 14 eqeltrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 0g ‘ 𝐻 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) )
16 15 snssd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → { ( 0g ‘ 𝐻 ) } ⊆ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) )
17 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
18 17 mptpreima ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) “ { ( 0g ‘ 𝐻 ) } ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ { ( 0g ‘ 𝐻 ) } }
19 nsgsubg ⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
20 19 3ad2ant2 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
21 eqid ⊢ ( 𝐺 ~QG 𝑌 ) = ( 𝐺 ~QG 𝑌 )
22 9 21 4 eqgid ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = 𝑌 )
23 20 22 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = 𝑌 )
24 9 subgss ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ ( Base ‘ 𝐺 ) )
25 20 24 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑌 ⊆ ( Base ‘ 𝐺 ) )
26 23 25 eqsstrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ⊆ ( Base ‘ 𝐺 ) )
27 sseqin2 ⊢ ( [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ⊆ ( Base ‘ 𝐺 ) ↔ ( ( Base ‘ 𝐺 ) ∩ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) )
28 26 27 sylib ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( Base ‘ 𝐺 ) ∩ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) )
29 9 21 eqger ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑌 ) Er ( Base ‘ 𝐺 ) )
30 20 29 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐺 ~QG 𝑌 ) Er ( Base ‘ 𝐺 ) )
31 30 11 erth ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 0g ‘ 𝐺 ) ( 𝐺 ~QG 𝑌 ) 𝑥 ↔ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) )
32 31 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( 𝐺 ~QG 𝑌 ) 𝑥 ↔ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) )
33 6 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = ( 0g ‘ 𝐻 ) )
34 33 eqeq1d ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ↔ ( 0g ‘ 𝐻 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) )
35 32 34 bitrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( 𝐺 ~QG 𝑌 ) 𝑥 ↔ ( 0g ‘ 𝐻 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) )
36 vex ⊢ 𝑥 ∈ V
37 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
38 36 37 elec ⊢ ( 𝑥 ∈ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ↔ ( 0g ‘ 𝐺 ) ( 𝐺 ~QG 𝑌 ) 𝑥 )
39 fvex ⊢ ( 0g ‘ 𝐻 ) ∈ V
40 39 elsn2 ⊢ ( [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ { ( 0g ‘ 𝐻 ) } ↔ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = ( 0g ‘ 𝐻 ) )
41 eqcom ⊢ ( [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = ( 0g ‘ 𝐻 ) ↔ ( 0g ‘ 𝐻 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
42 40 41 bitri ⊢ ( [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ { ( 0g ‘ 𝐻 ) } ↔ ( 0g ‘ 𝐻 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
43 35 38 42 3bitr4g ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ↔ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ { ( 0g ‘ 𝐻 ) } ) )
44 43 rabbi2dva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( Base ‘ 𝐺 ) ∩ [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑌 ) ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ { ( 0g ‘ 𝐻 ) } } )
45 28 44 23 3eqtr3d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ { ( 0g ‘ 𝐻 ) } } = 𝑌 )
46 18 45 syl5eq ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) “ { ( 0g ‘ 𝐻 ) } ) = 𝑌 )
47 simp3 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑌 ∈ ( Clsd ‘ 𝐽 ) )
48 46 47 eqeltrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) “ { ( 0g ‘ 𝐻 ) } ) ∈ ( Clsd ‘ 𝐽 ) )
49 2 9 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
50 49 3ad2ant1 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
51 1 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) ) )
52 eqidd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
53 12 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐺 ~QG 𝑌 ) ∈ V )
54 simp1 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐺 ∈ TopGrp )
55 51 52 17 53 54 quslem ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) : ( Base ‘ 𝐺 ) –onto→ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) )
56 qtopcld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) : ( Base ‘ 𝐺 ) –onto→ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) ) → ( { ( 0g ‘ 𝐻 ) } ∈ ( Clsd ‘ ( 𝐽 qTop ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) ) ) ↔ ( { ( 0g ‘ 𝐻 ) } ⊆ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) ∧ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) “ { ( 0g ‘ 𝐻 ) } ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
57 50 55 56 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( { ( 0g ‘ 𝐻 ) } ∈ ( Clsd ‘ ( 𝐽 qTop ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) ) ) ↔ ( { ( 0g ‘ 𝐻 ) } ⊆ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑌 ) ) ∧ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) “ { ( 0g ‘ 𝐻 ) } ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
58 16 48 57 mpbir2and ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → { ( 0g ‘ 𝐻 ) } ∈ ( Clsd ‘ ( 𝐽 qTop ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) ) ) )
59 51 52 17 53 54 qusval ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐻 = ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) “s 𝐺 ) )
60 59 52 55 54 2 3 imastopn ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐾 = ( 𝐽 qTop ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) ) )
61 60 fveq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( Clsd ‘ 𝐾 ) = ( Clsd ‘ ( 𝐽 qTop ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ) ) ) )
62 58 61 eleqtrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → { ( 0g ‘ 𝐻 ) } ∈ ( Clsd ‘ 𝐾 ) )
63 1 qustgp ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopGrp )
64 63 3adant3 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐻 ∈ TopGrp )
65 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
66 65 3 tgphaus ⊢ ( 𝐻 ∈ TopGrp → ( 𝐾 ∈ Haus ↔ { ( 0g ‘ 𝐻 ) } ∈ ( Clsd ‘ 𝐾 ) ) )
67 64 66 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐾 ∈ Haus ↔ { ( 0g ‘ 𝐻 ) } ∈ ( Clsd ‘ 𝐾 ) ) )
68 62 67 mpbird ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐾 ∈ Haus )