Theorem tgphaus 22412

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 22374	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2		eqid 2797	. . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺)
3		tgphaus.1	. . . . . 6 ⊢ 0 = (0g‘𝐺)
4	2, 3	grpidcl 17893	. . . . 5 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
5	1, 4	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6		tgphaus.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
7	6, 2	tgptopon 22378	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8		toponuni 21210	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽)
9	7, 8	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → (Base‘𝐺) = ∪ 𝐽)
10	5, 9	eleqtrd 2887	. . 3 ⊢ (𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽)
11		eqid 2797	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
12	11	sncld 21667	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 0 ∈ ∪ 𝐽) → { 0 } ∈ (Clsd‘𝐽))
13	12	expcom 414	. . 3 ⊢ ( 0 ∈ ∪ 𝐽 → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
14	10, 13	syl 17	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
15		eqid 2797	. . . . . 6 ⊢ (-g‘𝐺) = (-g‘𝐺)
16	6, 15	tgpsubcn 22386	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17		cnclima 21564	. . . . . 6 ⊢ (((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)))
18	17	ex 413	. . . . 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 5832	. . . . . . . . 9 ⊢ (◡(-g‘𝐺) “ { 0 }) ⊆ dom (-g‘𝐺)
21	2, 15	grpsubf 17939	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
22	1, 21	syl 17	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
23	20, 22	fssdm 6405	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
24		relxp 5468	. . . . . . . 8 ⊢ Rel ((Base‘𝐺) × (Base‘𝐺))
25		relss 5549	. . . . . . . 8 ⊢ ((◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel (◡(-g‘𝐺) “ { 0 })))
26	23, 24, 25	mpisyl 21	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → Rel (◡(-g‘𝐺) “ { 0 }))
27		dfrel4v 5930	. . . . . . 7 ⊢ (Rel (◡(-g‘𝐺) “ { 0 }) ↔ (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
28	26, 27	sylib 219	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
29	22	ffnd 6390	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
30		elpreima 6700	. . . . . . . . . . 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 5486	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
33	32	anbi1i 623	. . . . . . . . . . 11 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
34	2, 3, 15	grpsubeq0 17946	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
35	34	3expb 1113	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
36	1, 35	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
37		df-ov 7026	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘⟨𝑥, 𝑦⟩)
38	37	eleq1i 2875	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
39		ovex 7055	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) ∈ V
40	39	elsn 4493	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
41	38, 40	bitr3i 278	. . . . . . . . . . . . 13 ⊢ (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
42		equcom 2006	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
43	36, 41, 42	3bitr4g 315	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ 𝑦 = 𝑥))
44	43	pm5.32da 579	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
45	33, 44	syl5bb 284	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
46	31, 45	bitrd 280	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
47		df-br 4969	. . . . . . . . 9 ⊢ (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }))
48		eleq1w 2867	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺)))
49	48	biimparc 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺))
50	49	pm4.71i 560	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
51		an32 642	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
52	50, 51	bitr4i 279	. . . . . . . . 9 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))
53	46, 47, 52	3bitr4g 315	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)))
54	53	opabbidv 5034	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
55		opabresid 5804	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)} = ( I ↾ (Base‘𝐺))
56	54, 55	syl6eq 2849	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
57	9	reseq2d 5741	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ ∪ 𝐽))
58	28, 56, 57	3eqtrd 2837	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = ( I ↾ ∪ 𝐽))
59	58	eleq1d 2869	. . . 4 ⊢ (𝐺 ∈ TopGrp → ((◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
60	19, 59	sylibd 240	. . 3 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
61		topontop 21209	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
62	7, 61	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
63	11	hausdiag 21941	. . . . 5 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
64	63	baib 536	. . . 4 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
65	62, 64	syl 17	. . 3 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
66	60, 65	sylibrd 260	. 2 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → 𝐽 ∈ Haus))
67	14, 66	impbid 213	1 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1525   ∈ wcel 2083   ⊆ wss 3865  {csn 4478  ⟨cop 4484  ∪ cuni 4751   class class class wbr 4968  {copab 5030   I cid 5354   × cxp 5448  ^◡ccnv 5449   ↾ cres 5452   “ cima 5453  Rel wrel 5455   Fn wfn 6227  ⟶wf 6228  ‘cfv 6232  (class class class)co 7023  Basecbs 16316  TopOpenctopn 16528  0_gc0g 16546  Grpcgrp 17865  -_gcsg 17867  Topctop 21189  TopOnctopon 21206  Clsdccld 21312   Cn ccn 21520  Hauscha 21604   ×_t ctx 21856  TopGrpctgp 22367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-fo 6238  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-1st 7552  df-2nd 7553  df-map 8265  df-0g 16548  df-topgen 16550  df-plusf 17684  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-grp 17868  df-minusg 17869  df-sbg 17870  df-top 21190  df-topon 21207  df-topsp 21229  df-bases 21242  df-cld 21315  df-cn 21523  df-t1 21610  df-haus 21611  df-tx 21858  df-tmd 22368  df-tgp 22369

This theorem is referenced by:  tgpt1  22413  qustgphaus  22418