Theorem tgphaus 21730

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 21692	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
2		eqid 2610	. . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺)
3		tgphaus.1	. . . . . 6 ⊢ 0 = (0g‘𝐺)
4	2, 3	grpidcl 17273	. . . . 5 ⊢ (𝐺 ∈ Grp → 0 ∈ (Base‘𝐺))
5	1, 4	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → 0 ∈ (Base‘𝐺))
6		tgphaus.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
7	6, 2	tgptopon 21696	. . . . 5 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
8		toponuni 20542	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽)
9	7, 8	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → (Base‘𝐺) = ∪ 𝐽)
10	5, 9	eleqtrd 2690	. . 3 ⊢ (𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽)
11		eqid 2610	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
12	11	sncld 20985	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ 0 ∈ ∪ 𝐽) → { 0 } ∈ (Clsd‘𝐽))
13	12	expcom 450	. . 3 ⊢ ( 0 ∈ ∪ 𝐽 → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
14	10, 13	syl 17	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈ (Clsd‘𝐽)))
15		eqid 2610	. . . . . 6 ⊢ (-g‘𝐺) = (-g‘𝐺)
16	6, 15	tgpsubcn 21704	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
17		cnclima 20882	. . . . . 6 ⊢ (((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → (◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)))
18	17	ex 449	. . . . 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 5404	. . . . . . . . 9 ⊢ (◡(-g‘𝐺) “ { 0 }) ⊆ dom (-g‘𝐺)
21	2, 15	grpsubf 17317	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
22	1, 21	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
23		fdm 5964	. . . . . . . . . 10 ⊢ ((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → dom (-g‘𝐺) = ((Base‘𝐺) × (Base‘𝐺)))
24	22, 23	syl 17	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → dom (-g‘𝐺) = ((Base‘𝐺) × (Base‘𝐺)))
25	20, 24	syl5sseq 3616	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
26		relxp 5150	. . . . . . . 8 ⊢ Rel ((Base‘𝐺) × (Base‘𝐺))
27		relss 5129	. . . . . . . 8 ⊢ ((◡(-g‘𝐺) “ { 0 }) ⊆ ((Base‘𝐺) × (Base‘𝐺)) → (Rel ((Base‘𝐺) × (Base‘𝐺)) → Rel (◡(-g‘𝐺) “ { 0 })))
28	25, 26, 27	mpisyl 21	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → Rel (◡(-g‘𝐺) “ { 0 }))
29		dfrel4v 5503	. . . . . . 7 ⊢ (Rel (◡(-g‘𝐺) “ { 0 }) ↔ (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
30	28, 29	sylib 207	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦})
31		ffn 5958	. . . . . . . . . . . 12 ⊢ ((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
32	22, 31	syl 17	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
33		elpreima 6245	. . . . . . . . . . 11 ⊢ ((-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })))
35		opelxp 5070	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
36	35	anbi1i 727	. . . . . . . . . . 11 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }))
37	2, 3, 15	grpsubeq0 17324	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
38	37	3expb 1258	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
39	1, 38	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦))
40		df-ov 6552	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘⟨𝑥, 𝑦⟩)
41	40	eleq1i 2679	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 })
42		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ (𝑥(-g‘𝐺)𝑦) ∈ V
43	42	elsn 4140	. . . . . . . . . . . . . 14 ⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
44	41, 43	bitr3i 265	. . . . . . . . . . . . 13 ⊢ (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 )
45		equcom 1932	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
46	39, 44, 45	3bitr4g 302	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 } ↔ 𝑦 = 𝑥))
47	46	pm5.32da 671	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
48	36, 47	syl5bb 271	. . . . . . . . . 10 ⊢ (𝐺 ∈ TopGrp → ((⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘⟨𝑥, 𝑦⟩) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
49	34, 48	bitrd 267	. . . . . . . . 9 ⊢ (𝐺 ∈ TopGrp → (⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)))
50		df-br 4584	. . . . . . . . 9 ⊢ (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (◡(-g‘𝐺) “ { 0 }))
51		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺)))
52	51	biimparc 503	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺))
53	52	pm4.71i 662	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
54		an32 835	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺)))
55	53, 54	bitr4i 266	. . . . . . . . 9 ⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))
56	49, 50, 55	3bitr4g 302	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)))
57	56	opabbidv 4648	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)})
58		opabresid 5374	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)} = ( I ↾ (Base‘𝐺))
59	57, 58	syl6eq 2660	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → {⟨𝑥, 𝑦⟩ ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺)))
60	9	reseq2d 5317	. . . . . 6 ⊢ (𝐺 ∈ TopGrp → ( I ↾ (Base‘𝐺)) = ( I ↾ ∪ 𝐽))
61	30, 59, 60	3eqtrd 2648	. . . . 5 ⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = ( I ↾ ∪ 𝐽))
62	61	eleq1d 2672	. . . 4 ⊢ (𝐺 ∈ TopGrp → ((◡(-g‘𝐺) “ { 0 }) ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
63	19, 62	sylibd 228	. . 3 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
64		topontop 20541	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
65	7, 64	syl 17	. . . 4 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ Top)
66	11	hausdiag 21258	. . . . 5 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
67	66	baib 942	. . . 4 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
68	65, 67	syl 17	. . 3 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽))))
69	63, 68	sylibrd 248	. 2 ⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈ (Clsd‘𝐽) → 𝐽 ∈ Haus))
70	14, 69	impbid 201	1 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈ (Clsd‘𝐽)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540  {csn 4125  ⟨cop 4131  ∪ cuni 4372   class class class wbr 4583  {copab 4642   I cid 4948   × cxp 5036  ^◡ccnv 5037  dom cdm 5038   ↾ cres 5040   “ cima 5041  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  TopOpenctopn 15905  0_gc0g 15923  Grpcgrp 17245  -_gcsg 17247  Topctop 20517  TopOnctopon 20518  Clsdccld 20630   Cn ccn 20838  Hauscha 20922   ×_t ctx 21173  TopGrpctgp 21685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-0g 15925  df-topgen 15927  df-plusf 17064  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-sbg 17250  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-cn 20841  df-t1 20928  df-haus 20929  df-tx 21175  df-tmd 21686  df-tgp 21687

This theorem is referenced by:  tgpt1  21731  qustgphaus  21736