Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgphaus Structured version   Visualization version   GIF version

Theorem tgphaus 22729
 Description: A topological group is Hausdorff iff the identity subgroup is closed. (Contributed by Mario Carneiro, 18-Sep-2015.)
Hypotheses
Ref Expression
tgphaus.1 0 = (0g𝐺)
tgphaus.j 𝐽 = (TopOpen‘𝐺)
Assertion
Ref Expression
tgphaus (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))

Proof of Theorem tgphaus
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tgpgrp 22690 . . . . 5 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2 eqid 2798 . . . . . 6 (Base‘𝐺) = (Base‘𝐺)
3 tgphaus.1 . . . . . 6 0 = (0g𝐺)
42, 3grpidcl 18126 . . . . 5 (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
51, 4syl 17 . . . 4 (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6 tgphaus.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
76, 2tgptopon 22694 . . . . 5 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8 toponuni 21526 . . . . 5 (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = 𝐽)
97, 8syl 17 . . . 4 (𝐺 ∈ TopGrp → (Base‘𝐺) = 𝐽)
105, 9eleqtrd 2892 . . 3 (𝐺 ∈ TopGrp → 0 𝐽)
11 eqid 2798 . . . . 5 𝐽 = 𝐽
1211sncld 21983 . . . 4 ((𝐽 ∈ Haus ∧ 0 𝐽) → { 0 } ∈ (Clsd‘𝐽))
1312expcom 417 . . 3 ( 0 𝐽 → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
1410, 13syl 17 . 2 (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
15 eqid 2798 . . . . . 6 (-g𝐺) = (-g𝐺)
166, 15tgpsubcn 22702 . . . . 5 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17 cnclima 21880 . . . . . 6 (((-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → ((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)))
1817ex 416 . . . . 5 ((-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) → ({ 0 } ∈ (Clsd‘𝐽) → ((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
1916, 18syl 17 . . . 4 (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
20 cnvimass 5916 . . . . . . . . 9 ((-g𝐺) “ { 0 }) ⊆ dom (-g𝐺)
212, 15grpsubf 18173 . . . . . . . . . 10 (𝐺 ∈ Grp → (-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
221, 21syl 17 . . . . . . . . 9 (𝐺 ∈ TopGrp → (-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
2320, 22fssdm 6504 . . . . . . . 8 (𝐺 ∈ TopGrp → ((-g𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
24 relxp 5537 . . . . . . . 8 Rel ((Base‘𝐺) × (Base‘𝐺))
25 relss 5620 . . . . . . . 8 (((-g𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel ((-g𝐺) “ { 0 })))
2623, 24, 25mpisyl 21 . . . . . . 7 (𝐺 ∈ TopGrp → Rel ((-g𝐺) “ { 0 }))
27 dfrel4v 6014 . . . . . . 7 (Rel ((-g𝐺) “ { 0 }) ↔ ((-g𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦})
2826, 27sylib 221 . . . . . 6 (𝐺 ∈ TopGrp → ((-g𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦})
2922ffnd 6488 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
30 elpreima 6805 . . . . . . . . . . 11 ((-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
3129, 30syl 17 . . . . . . . . . 10 (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
32 opelxp 5555 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
3332anbi1i 626 . . . . . . . . . . 11 ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
342, 3, 15grpsubeq0 18180 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g𝐺)𝑦) = 0𝑥 = 𝑦))
35343expb 1117 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g𝐺)𝑦) = 0𝑥 = 𝑦))
361, 35sylan 583 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g𝐺)𝑦) = 0𝑥 = 𝑦))
37 df-ov 7138 . . . . . . . . . . . . . . 15 (𝑥(-g𝐺)𝑦) = ((-g𝐺)‘⟨𝑥, 𝑦⟩)
3837eleq1i 2880 . . . . . . . . . . . . . 14 ((𝑥(-g𝐺)𝑦) ∈ { 0 } ↔ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
39 ovex 7168 . . . . . . . . . . . . . . 15 (𝑥(-g𝐺)𝑦) ∈ V
4039elsn 4540 . . . . . . . . . . . . . 14 ((𝑥(-g𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g𝐺)𝑦) = 0 )
4138, 40bitr3i 280 . . . . . . . . . . . . 13 (((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g𝐺)𝑦) = 0 )
42 equcom 2025 . . . . . . . . . . . . 13 (𝑦 = 𝑥𝑥 = 𝑦)
4336, 41, 423bitr4g 317 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ 𝑦 = 𝑥))
4443pm5.32da 582 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
4533, 44syl5bb 286 . . . . . . . . . 10 (𝐺 ∈ TopGrp → ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
4631, 45bitrd 282 . . . . . . . . 9 (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
47 df-br 5031 . . . . . . . . 9 (𝑥((-g𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }))
48 eleq1w 2872 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺)))
4948biimparc 483 . . . . . . . . . . 11 ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺))
5049pm4.71i 563 . . . . . . . . . 10 ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
51 an32 645 . . . . . . . . . 10 (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
5250, 51bitr4i 281 . . . . . . . . 9 ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))
5346, 47, 523bitr4g 317 . . . . . . . 8 (𝐺 ∈ TopGrp → (𝑥((-g𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)))
5453opabbidv 5096 . . . . . . 7 (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
55 opabresid 5884 . . . . . . 7 ( I ↾ (Base‘𝐺)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)}
5654, 55eqtr4di 2851 . . . . . 6 (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
579reseq2d 5818 . . . . . 6 (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ 𝐽))
5828, 56, 573eqtrd 2837 . . . . 5 (𝐺 ∈ TopGrp → ((-g𝐺) “ { 0 }) = ( I ↾ 𝐽))
5958eleq1d 2874 . . . 4 (𝐺 ∈ TopGrp → (((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6019, 59sylibd 242 . . 3 (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
61 topontop 21525 . . . . 5 (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
627, 61syl 17 . . . 4 (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
6311hausdiag 22257 . . . . 5 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6463baib 539 . . . 4 (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6562, 64syl 17 . . 3 (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6660, 65sylibrd 262 . 2 (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → 𝐽 ∈ Haus))
6714, 66impbid 215 1 (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  {csn 4525  ⟨cop 4531  ∪ cuni 4800   class class class wbr 5030  {copab 5092   I cid 5424   × cxp 5517  ◡ccnv 5518   ↾ cres 5521   “ cima 5522  Rel wrel 5524   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  Basecbs 16477  TopOpenctopn 16689  0gc0g 16707  Grpcgrp 18097  -gcsg 18099  Topctop 21505  TopOnctopon 21522  Clsdccld 21628   Cn ccn 21836  Hauscha 21920   ×t ctx 22172  TopGrpctgp 22683 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fo 6330  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7673  df-2nd 7674  df-map 8393  df-0g 16709  df-topgen 16711  df-plusf 17845  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-grp 18100  df-minusg 18101  df-sbg 18102  df-top 21506  df-topon 21523  df-topsp 21545  df-bases 21558  df-cld 21631  df-cn 21839  df-t1 21926  df-haus 21927  df-tx 22174  df-tmd 22684  df-tgp 22685 This theorem is referenced by:  tgpt1  22730  qustgphaus  22735
 Copyright terms: Public domain W3C validator