Theorem tgphaus 24466

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.

Step	Hyp	Ref	Expression
1		tgpgrp 24427	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2		eqid 2763	. . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺)
3		tgphaus.1	. . . . . 6 ⊢ 0 = (0g‘𝐺)
4	2, 3	grpidcl 19205	. . . . 5 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
5	1, 4	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6		tgphaus.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
7	6, 2	tgptopon 24431	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8		toponuni 23262	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽)
9	7, 8	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → (Base‘𝐺) = ∪ 𝐽)
10	5, 9	eleqtrd 2866	. . 3 ⊢ (𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽)
11		eqid 2763	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
12	11	sncld 23719	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 0 ∈ ∪ 𝐽) → { 0 } ∈ (Clsd‘𝐽))
13	12	expcom 419	. . 3 ⊢ ( 0 ∈ ∪ 𝐽 → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
14	10, 13	syl 18	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
15		eqid 2763	. . . . . 6 ⊢ (-g‘𝐺) = (-g‘𝐺)
16	6, 15	tgpsubcn 24439	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17		cnclima 23616	. . . . . 6 ⊢ (((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)))
18	17	ex 418	. . . . 5 ⊢ ((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) → ({ 0 } ∈ (Clsd‘𝐽) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
19	16, 18	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
20		cnvimass 6211	. . . . . . . . 9 ⊢ (◡(-g‘𝐺) “ { 0 }) ⊆ dom (-g‘𝐺)
21	2, 15	grpsubf 19258	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
22	1, 21	syl 18	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
23	20, 22	fssdm 6751	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
24		relxp 5673	. . . . . . . 8 ⊢ Rel ((Base‘𝐺) × (Base‘𝐺))
25		relss 5763	. . . . . . . 8 ⊢ ((◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel (◡(-g‘𝐺) “ { 0 })))
26	23, 24, 25	mpisyl 22	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → Rel (◡(-g‘𝐺) “ { 0 }))
27		dfrel4v 6194	. . . . . . 7 ⊢ (Rel (◡(-g‘𝐺) “ { 0 }) ↔ (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
28	26, 27	sylib 221	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
29	22	ffnd 6732	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
30		elpreima 7080	. . . . . . . . . . 11 ⊢ ((-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
31	29, 30	syl 18	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
32		opelxp 5691	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
33	32	anbi1i 636	. . . . . . . . . . 11 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
34	2, 3, 15	grpsubeq0 19265	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
35	34	3expb 1138	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
36	1, 35	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
37		df-ov 7446	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘⟨𝑥, 𝑦⟩)
38	37	eleq1i 2855	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
39		ovex 7476	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) ∈ V
40	39	elsn 4599	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
41	38, 40	bitr3i 280	. . . . . . . . . . . . 13 ⊢ (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
42		equcom 2053	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
43	36, 41, 42	3bitr4g 317	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ 𝑦 = 𝑥))
44	43	pm5.32da 590	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
45	33, 44	bitrid 286	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
46	31, 45	bitrd 282	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
47		df-br 5107	. . . . . . . . 9 ⊢ (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }))
48		eleq1w 2847	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺)))
49	48	biimparc 485	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺))
50	49	pm4.71i 569	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
51		an32 659	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
52	50, 51	bitr4i 281	. . . . . . . . 9 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))
53	46, 47, 52	3bitr4g 317	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)))
54	53	opabbidv 5174	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
55		opabresid 6054	. . . . . . 7 ⊢ ( I ↾ (Base‘𝐺)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)}
56	54, 55	eqtr4di 2816	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
57	9	reseq2d 5981	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ ∪ 𝐽))
58	28, 56, 57	3eqtrd 2802	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = ( I ↾ ∪ 𝐽))
59	58	eleq1d 2849	. . . 4 ⊢ (𝐺 ∈ TopGrp → ((◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
60	19, 59	sylibd 242	. . 3 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
61		topontop 23261	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
62	7, 61	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
63	11	hausdiag 23994	. . . . 5 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
64	63	baib 545	. . . 4 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
65	62, 64	syl 18	. . 3 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
66	60, 65	sylibrd 262	. 2 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → 𝐽 ∈ Haus))
67	14, 66	impbid 215	1 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  {csn 4588  ⟨cop 4838  ∪ cuni 4870   class class class wbr 5106  {copab 5170   I cid 5549   × cxp 5653  ^◡ccnv 5654   ↾ cres 5657   “ cima 5658  Rel wrel 5660   Fn wfn 6553  ⟶wf 6554  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  TopOpenctopn 17621  0_gc0g 17639  Grpcgrp 19173  -_gcsg 19175  Topctop 23241  TopOnctopon 23258  Clsdccld 23364   Cn ccn 23572  Hauscha 23656   ×_t ctx 23909  TopGrpctgp 24420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fo 6564  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1st 8025  df-2nd 8026  df-map 8877  df-0g 17641  df-topgen 17643  df-plusf 18844  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176  df-minusg 19177  df-sbg 19178  df-top 23242  df-topon 23259  df-topsp 23281  df-bases 23294  df-cld 23367  df-cn 23575  df-t1 23662  df-haus 23663  df-tx 23911  df-tmd 24421  df-tgp 24422

This theorem is used by:  tgpt1  24467  qustgphaus  24472