Metamath Proof Explorer

Theorem tgphaus

Description: A topological group is Hausdorff iff the identity subgroup is closed. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tgphaus.1 ⊢ 0 = ( 0g ‘ 𝐺 )
tgphaus.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion tgphaus ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ { 0 } ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 tgphaus.1 ⊢ 0 = ( 0g ‘ 𝐺 )
2 tgphaus.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 4 1 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
6 3 5 syl ⊢ ( 𝐺 ∈ TopGrp → 0 ∈ ( Base ‘ 𝐺 ) )
7 2 4 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
8 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
9 7 8 syl ⊢ ( 𝐺 ∈ TopGrp → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
10 6 9 eleqtrd ⊢ ( 𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽 )
11 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
12 11 sncld ⊢ ( ( 𝐽 ∈ Haus ∧ 0 ∈ ∪ 𝐽 ) → { 0 } ∈ ( Clsd ‘ 𝐽 ) )
13 12 expcom ⊢ ( 0 ∈ ∪ 𝐽 → ( 𝐽 ∈ Haus → { 0 } ∈ ( Clsd ‘ 𝐽 ) ) )
14 10 13 syl ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus → { 0 } ∈ ( Clsd ‘ 𝐽 ) ) )
15 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
16 2 15 tgpsubcn ⊢ ( 𝐺 ∈ TopGrp → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
17 cnclima ⊢ ( ( ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ { 0 } ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
18 17 ex ⊢ ( ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) → ( { 0 } ∈ ( Clsd ‘ 𝐽 ) → ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
19 16 18 syl ⊢ ( 𝐺 ∈ TopGrp → ( { 0 } ∈ ( Clsd ‘ 𝐽 ) → ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
20 cnvimass ⊢ ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ⊆ dom ( -g ‘ 𝐺 )
21 4 15 grpsubf ⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) )
22 3 21 syl ⊢ ( 𝐺 ∈ TopGrp → ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) )
23 20 22 fssdm ⊢ ( 𝐺 ∈ TopGrp → ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
24 relxp ⊢ Rel ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) )
25 relss ⊢ ( ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) → ( Rel ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) → Rel ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ) )
26 23 24 25 mpisyl ⊢ ( 𝐺 ∈ TopGrp → Rel ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) )
27 dfrel4v ⊢ ( Rel ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ↔ ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) 𝑦 } )
28 26 27 sylib ⊢ ( 𝐺 ∈ TopGrp → ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) 𝑦 } )
29 22 ffnd ⊢ ( 𝐺 ∈ TopGrp → ( -g ‘ 𝐺 ) Fn ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
30 elpreima ⊢ ( ( -g ‘ 𝐺 ) Fn ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ) ) )
31 29 30 syl ⊢ ( 𝐺 ∈ TopGrp → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ) ) )
32 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) )
33 32 anbi1i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ) )
34 4 1 15 grpsubeq0 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
35 34 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
36 3 35 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
37 df-ov ⊢ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
38 37 eleq1i ⊢ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ { 0 } ↔ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } )
39 ovex ⊢ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ V
40 39 elsn ⊢ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ { 0 } ↔ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = 0 )
41 38 40 bitr3i ⊢ ( ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ↔ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = 0 )
42 equcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
43 36 41 42 3bitr4g ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ↔ 𝑦 = 𝑥 ) )
44 43 pm5.32da ⊢ ( 𝐺 ∈ TopGrp → ( ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 = 𝑥 ) ) )
45 33 44 syl5bb ⊢ ( 𝐺 ∈ TopGrp → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ { 0 } ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 = 𝑥 ) ) )
46 31 45 bitrd ⊢ ( 𝐺 ∈ TopGrp → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 = 𝑥 ) ) )
47 df-br ⊢ ( 𝑥 ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) )
48 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↔ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
49 48 biimparc ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
50 49 pm4.71i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) )
51 an32 ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) )
52 50 51 bitr4i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 = 𝑥 ) )
53 46 47 52 3bitr4g ⊢ ( 𝐺 ∈ TopGrp → ( 𝑥 ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) 𝑦 ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) ) )
54 53 opabbidv ⊢ ( 𝐺 ∈ TopGrp → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) } )
55 opabresid ⊢ ( I ↾ ( Base ‘ 𝐺 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 = 𝑥 ) }
56 54 55 eqtr4di ⊢ ( 𝐺 ∈ TopGrp → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) 𝑦 } = ( I ↾ ( Base ‘ 𝐺 ) ) )
57 9 reseq2d ⊢ ( 𝐺 ∈ TopGrp → ( I ↾ ( Base ‘ 𝐺 ) ) = ( I ↾ ∪ 𝐽 ) )
58 28 56 57 3eqtrd ⊢ ( 𝐺 ∈ TopGrp → ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) = ( I ↾ ∪ 𝐽 ) )
59 58 eleq1d ⊢ ( 𝐺 ∈ TopGrp → ( ( ◡ ( -g ‘ 𝐺 ) “ { 0 } ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ↔ ( I ↾ ∪ 𝐽 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
60 19 59 sylibd ⊢ ( 𝐺 ∈ TopGrp → ( { 0 } ∈ ( Clsd ‘ 𝐽 ) → ( I ↾ ∪ 𝐽 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
61 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
62 7 61 syl ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ Top )
63 11 hausdiag ⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ( I ↾ ∪ 𝐽 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
64 63 baib ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
65 62 64 syl ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
66 60 65 sylibrd ⊢ ( 𝐺 ∈ TopGrp → ( { 0 } ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Haus ) )
67 14 66 impbid ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ { 0 } ∈ ( Clsd ‘ 𝐽 ) ) )