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

Theorem tgphaus 21967
 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 21929 . . . . 5 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2 eqid 2651 . . . . . 6 (Base‘𝐺) = (Base‘𝐺)
3 tgphaus.1 . . . . . 6 0 = (0g𝐺)
42, 3grpidcl 17497 . . . . 5 (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
51, 4syl 17 . . . 4 (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6 tgphaus.j . . . . . 6 𝐽 = (TopOpen‘𝐺)
76, 2tgptopon 21933 . . . . 5 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8 toponuni 20767 . . . . 5 (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = 𝐽)
97, 8syl 17 . . . 4 (𝐺 ∈ TopGrp → (Base‘𝐺) = 𝐽)
105, 9eleqtrd 2732 . . 3 (𝐺 ∈ TopGrp → 0 𝐽)
11 eqid 2651 . . . . 5 𝐽 = 𝐽
1211sncld 21223 . . . 4 ((𝐽 ∈ Haus ∧ 0 𝐽) → { 0 } ∈ (Clsd‘𝐽))
1312expcom 450 . . 3 ( 0 𝐽 → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
1410, 13syl 17 . 2 (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
15 eqid 2651 . . . . . 6 (-g𝐺) = (-g𝐺)
166, 15tgpsubcn 21941 . . . . 5 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17 cnclima 21120 . . . . . 6 (((-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → ((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)))
1817ex 449 . . . . 5 ((-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) → ({ 0 } ∈ (Clsd‘𝐽) → ((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
1916, 18syl 17 . . . 4 (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
20 cnvimass 5520 . . . . . . . . 9 ((-g𝐺) “ { 0 }) ⊆ dom (-g𝐺)
212, 15grpsubf 17541 . . . . . . . . . . 11 (𝐺 ∈ Grp → (-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
221, 21syl 17 . . . . . . . . . 10 (𝐺 ∈ TopGrp → (-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
23 fdm 6089 . . . . . . . . . 10 ((-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → dom (-g𝐺) = ((Base‘𝐺) × (Base‘𝐺)))
2422, 23syl 17 . . . . . . . . 9 (𝐺 ∈ TopGrp → dom (-g𝐺) = ((Base‘𝐺) × (Base‘𝐺)))
2520, 24syl5sseq 3686 . . . . . . . 8 (𝐺 ∈ TopGrp → ((-g𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
26 relxp 5160 . . . . . . . 8 Rel ((Base‘𝐺) × (Base‘𝐺))
27 relss 5240 . . . . . . . 8 (((-g𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel ((-g𝐺) “ { 0 })))
2825, 26, 27mpisyl 21 . . . . . . 7 (𝐺 ∈ TopGrp → Rel ((-g𝐺) “ { 0 }))
29 dfrel4v 5619 . . . . . . 7 (Rel ((-g𝐺) “ { 0 }) ↔ ((-g𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦})
3028, 29sylib 208 . . . . . 6 (𝐺 ∈ TopGrp → ((-g𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦})
31 ffn 6083 . . . . . . . . . . . 12 ((-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → (-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
3222, 31syl 17 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
33 elpreima 6377 . . . . . . . . . . 11 ((-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
3432, 33syl 17 . . . . . . . . . 10 (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
35 opelxp 5180 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
3635anbi1i 731 . . . . . . . . . . 11 ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
372, 3, 15grpsubeq0 17548 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g𝐺)𝑦) = 0𝑥 = 𝑦))
38373expb 1285 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g𝐺)𝑦) = 0𝑥 = 𝑦))
391, 38sylan 487 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g𝐺)𝑦) = 0𝑥 = 𝑦))
40 df-ov 6693 . . . . . . . . . . . . . . 15 (𝑥(-g𝐺)𝑦) = ((-g𝐺)‘⟨𝑥, 𝑦⟩)
4140eleq1i 2721 . . . . . . . . . . . . . 14 ((𝑥(-g𝐺)𝑦) ∈ { 0 } ↔ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
42 ovex 6718 . . . . . . . . . . . . . . 15 (𝑥(-g𝐺)𝑦) ∈ V
4342elsn 4225 . . . . . . . . . . . . . 14 ((𝑥(-g𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g𝐺)𝑦) = 0 )
4441, 43bitr3i 266 . . . . . . . . . . . . 13 (((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g𝐺)𝑦) = 0 )
45 equcom 1991 . . . . . . . . . . . . 13 (𝑦 = 𝑥𝑥 = 𝑦)
4639, 44, 453bitr4g 303 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ 𝑦 = 𝑥))
4746pm5.32da 674 . . . . . . . . . . 11 (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
4836, 47syl5bb 272 . . . . . . . . . 10 (𝐺 ∈ TopGrp → ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
4934, 48bitrd 268 . . . . . . . . 9 (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
50 df-br 4686 . . . . . . . . 9 (𝑥((-g𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ { 0 }))
51 eleq1 2718 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺)))
5251biimparc 503 . . . . . . . . . . 11 ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺))
5352pm4.71i 665 . . . . . . . . . 10 ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
54 an32 856 . . . . . . . . . 10 (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
5553, 54bitr4i 267 . . . . . . . . 9 ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))
5649, 50, 553bitr4g 303 . . . . . . . 8 (𝐺 ∈ TopGrp → (𝑥((-g𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)))
5756opabbidv 4749 . . . . . . 7 (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
58 opabresid 5490 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)} = ( I ↾ (Base‘𝐺))
5957, 58syl6eq 2701 . . . . . 6 (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥((-g𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
609reseq2d 5428 . . . . . 6 (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ 𝐽))
6130, 59, 603eqtrd 2689 . . . . 5 (𝐺 ∈ TopGrp → ((-g𝐺) “ { 0 }) = ( I ↾ 𝐽))
6261eleq1d 2715 . . . 4 (𝐺 ∈ TopGrp → (((-g𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6319, 62sylibd 229 . . 3 (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
64 topontop 20766 . . . . 5 (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
657, 64syl 17 . . . 4 (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
6611hausdiag 21496 . . . . 5 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6766baib 964 . . . 4 (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6865, 67syl 17 . . 3 (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
6963, 68sylibrd 249 . 2 (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → 𝐽 ∈ Haus))
7014, 69impbid 202 1 (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ⊆ wss 3607  {csn 4210  ⟨cop 4216  ∪ cuni 4468   class class class wbr 4685  {copab 4745   I cid 5052   × cxp 5141  ◡ccnv 5142  dom cdm 5143   ↾ cres 5145   “ cima 5146  Rel wrel 5148   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  TopOpenctopn 16129  0gc0g 16147  Grpcgrp 17469  -gcsg 17471  Topctop 20746  TopOnctopon 20763  Clsdccld 20868   Cn ccn 21076  Hauscha 21160   ×t ctx 21411  TopGrpctgp 21922 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-0g 16149  df-topgen 16151  df-plusf 17288  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-grp 17472  df-minusg 17473  df-sbg 17474  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-cn 21079  df-t1 21166  df-haus 21167  df-tx 21413  df-tmd 21923  df-tgp 21924 This theorem is referenced by:  tgpt1  21968  qustgphaus  21973
 Copyright terms: Public domain W3C validator