Theorem tgphaus 24311

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 24272	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2		eqid 2766	. . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺)
3		tgphaus.1	. . . . . 6 ⊢ 0 = (0g‘𝐺)
4	2, 3	grpidcl 19063	. . . . 5 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
5	1, 4	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6		tgphaus.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
7	6, 2	tgptopon 24276	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8		toponuni 23108	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽)
9	7, 8	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → (Base‘𝐺) = ∪ 𝐽)
10	5, 9	eleqtrd 2868	. . 3 ⊢ (𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽)
11		eqid 2766	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
12	11	sncld 23565	. . . 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 2766	. . . . . 6 ⊢ (-g‘𝐺) = (-g‘𝐺)
16	6, 15	tgpsubcn 24284	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17		cnclima 23462	. . . . . 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 6089	. . . . . . . . 9 ⊢ (◡(-g‘𝐺) “ { 0 }) ⊆ dom (-g‘𝐺)
21	2, 15	grpsubf 19116	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
22	1, 21	syl 18	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
23	20, 22	fssdm 6732	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
24		relxp 5684	. . . . . . . 8 ⊢ Rel ((Base‘𝐺) × (Base‘𝐺))
25		relss 5773	. . . . . . . 8 ⊢ ((◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel (◡(-g‘𝐺) “ { 0 })))
26	23, 24, 25	mpisyl 22	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → Rel (◡(-g‘𝐺) “ { 0 }))
27		dfrel4v 6193	. . . . . . 7 ⊢ (Rel (◡(-g‘𝐺) “ { 0 }) ↔ (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
28	26, 27	sylib 221	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
29	22	ffnd 6713	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
30		elpreima 7060	. . . . . . . . . . 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 5702	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
33	32	anbi1i 636	. . . . . . . . . . 11 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
34	2, 3, 15	grpsubeq0 19123	. . . . . . . . . . . . . . 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 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘⟨𝑥, 𝑦⟩)
38	37	eleq1i 2857	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
39		ovex 7456	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) ∈ V
40	39	elsn 4609	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
41	38, 40	bitr3i 280	. . . . . . . . . . . . 13 ⊢ (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
42		equcom 2051	. . . . . . . . . . . . 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 5115	. . . . . . . . 9 ⊢ (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }))
48		eleq1w 2849	. . . . . . . . . . . 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 5182	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
55		opabresid 6057	. . . . . . 7 ⊢ ( I ↾ (Base‘𝐺)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)}
56	54, 55	eqtr4di 2819	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
57	9	reseq2d 5983	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ ∪ 𝐽))
58	28, 56, 57	3eqtrd 2805	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = ( I ↾ ∪ 𝐽))
59	58	eleq1d 2851	. . . 4 ⊢ (𝐺 ∈ TopGrp → ((◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
60	19, 59	sylibd 242	. . 3 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
61		topontop 23107	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
62	7, 61	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
63	11	hausdiag 23839	. . . . 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 2146   ⊆ wss 3908  {csn 4594  ⟨cop 4600  ∪ cuni 4877   class class class wbr 5114  {copab 5178   I cid 5560   × cxp 5664  ^◡ccnv 5665   ↾ cres 5668   “ cima 5669  Rel wrel 5671   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  TopOpenctopn 17499  0_gc0g 17517  Grpcgrp 19031  -_gcsg 19033  Topctop 23087  TopOnctopon 23104  Clsdccld 23210   Cn ccn 23418  Hauscha 23502   ×_t ctx 23754  TopGrpctgp 24265

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-map 8835  df-0g 17519  df-topgen 17521  df-plusf 18722  df-mgm 18723  df-sgrp 18806  df-mnd 18822  df-grp 19034  df-minusg 19035  df-sbg 19036  df-top 23088  df-topon 23105  df-topsp 23127  df-bases 23140  df-cld 23213  df-cn 23421  df-t1 23508  df-haus 23509  df-tx 23756  df-tmd 24266  df-tgp 24267

This theorem is used by:  tgpt1  24312  qustgphaus  24317