Theorem tgphaus 22213

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 22175	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2		eqid 2765	. . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺)
3		tgphaus.1	. . . . . 6 ⊢ 0 = (0g‘𝐺)
4	2, 3	grpidcl 17731	. . . . 5 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
5	1, 4	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6		tgphaus.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
7	6, 2	tgptopon 22179	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8		toponuni 21012	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽)
9	7, 8	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → (Base‘𝐺) = ∪ 𝐽)
10	5, 9	eleqtrd 2846	. . 3 ⊢ (𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽)
11		eqid 2765	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
12	11	sncld 21469	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 0 ∈ ∪ 𝐽) → { 0 } ∈ (Clsd‘𝐽))
13	12	expcom 402	. . 3 ⊢ ( 0 ∈ ∪ 𝐽 → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
14	10, 13	syl 17	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
15		eqid 2765	. . . . . 6 ⊢ (-g‘𝐺) = (-g‘𝐺)
16	6, 15	tgpsubcn 22187	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17		cnclima 21366	. . . . . 6 ⊢ (((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)))
18	17	ex 401	. . . . 5 ⊢ ((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) → ({ 0 } ∈ (Clsd‘𝐽) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
19	16, 18	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽))))
20		cnvimass 5669	. . . . . . . . 9 ⊢ (◡(-g‘𝐺) “ { 0 }) ⊆ dom (-g‘𝐺)
21	2, 15	grpsubf 17775	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
22	1, 21	syl 17	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
23	20, 22	fssdm 6241	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
24		relxp 5297	. . . . . . . 8 ⊢ Rel ((Base‘𝐺) × (Base‘𝐺))
25		relss 5378	. . . . . . . 8 ⊢ ((◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel (◡(-g‘𝐺) “ { 0 })))
26	23, 24, 25	mpisyl 21	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → Rel (◡(-g‘𝐺) “ { 0 }))
27		dfrel4v 5769	. . . . . . 7 ⊢ (Rel (◡(-g‘𝐺) “ { 0 }) ↔ (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
28	26, 27	sylib 209	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
29	22	ffnd 6226	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
30		elpreima 6531	. . . . . . . . . . 11 ⊢ ((-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
31	29, 30	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
32		opelxp 5315	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
33	32	anbi1i 617	. . . . . . . . . . 11 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
34	2, 3, 15	grpsubeq0 17782	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
35	34	3expb 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
36	1, 35	sylan 575	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
37		df-ov 6849	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘⟨𝑥, 𝑦⟩)
38	37	eleq1i 2835	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
39		ovex 6878	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) ∈ V
40	39	elsn 4351	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
41	38, 40	bitr3i 268	. . . . . . . . . . . . 13 ⊢ (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
42		equcom 2115	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
43	36, 41, 42	3bitr4g 305	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ 𝑦 = 𝑥))
44	43	pm5.32da 574	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
45	33, 44	syl5bb 274	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
46	31, 45	bitrd 270	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
47		df-br 4812	. . . . . . . . 9 ⊢ (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }))
48		eleq1w 2827	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺)))
49	48	biimparc 471	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺))
50	49	pm4.71i 555	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
51		an32 636	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
52	50, 51	bitr4i 269	. . . . . . . . 9 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))
53	46, 47, 52	3bitr4g 305	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)))
54	53	opabbidv 4877	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
55		opabresid 5641	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)} = ( I ↾ (Base‘𝐺))
56	54, 55	syl6eq 2815	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
57	9	reseq2d 5567	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ ∪ 𝐽))
58	28, 56, 57	3eqtrd 2803	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = ( I ↾ ∪ 𝐽))
59	58	eleq1d 2829	. . . 4 ⊢ (𝐺 ∈ TopGrp → ((◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
60	19, 59	sylibd 230	. . 3 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
61		topontop 21011	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
62	7, 61	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
63	11	hausdiag 21742	. . . . 5 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
64	63	baib 531	. . . 4 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
65	62, 64	syl 17	. . 3 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
66	60, 65	sylibrd 250	. 2 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → 𝐽 ∈ Haus))
67	14, 66	impbid 203	1 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1652   ∈ wcel 2155   ⊆ wss 3734  {csn 4336  ⟨cop 4342  ∪ cuni 4596   class class class wbr 4811  {copab 4873   I cid 5186   × cxp 5277  ^◡ccnv 5278   ↾ cres 5281   “ cima 5282  Rel wrel 5284   Fn wfn 6065  ⟶wf 6066  ‘cfv 6070  (class class class)co 6846  Basecbs 16144  TopOpenctopn 16362  0_gc0g 16380  Grpcgrp 17703  -_gcsg 17705  Topctop 20991  TopOnctopon 21008  Clsdccld 21114   Cn ccn 21322  Hauscha 21406   ×_t ctx 21657  TopGrpctgp 22168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-1st 7370  df-2nd 7371  df-map 8066  df-0g 16382  df-topgen 16384  df-plusf 17521  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-grp 17706  df-minusg 17707  df-sbg 17708  df-top 20992  df-topon 21009  df-topsp 21031  df-bases 21044  df-cld 21117  df-cn 21325  df-t1 21412  df-haus 21413  df-tx 21659  df-tmd 22169  df-tgp 22170

This theorem is referenced by:  tgpt1  22214  qustgphaus  22219