tgphaus

Description: A topological group is Hausdorff iff the identity subgroup is closed. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	tgphaus.1	$⊢ \underset{˙}{0} = 0_{G}$
	tgphaus.j	$⊢ J = TopOpen (G)$
Assertion	tgphaus	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow \{\underset{˙}{0}\} \in Clsd (J))$

Proof

Step	Hyp	Ref	Expression
1		tgphaus.1	$⊢ \underset{˙}{0} = 0_{G}$
2		tgphaus.j	$⊢ J = TopOpen (G)$
3		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	4 1	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in {Base}_{G}$
6	3 5	syl	$⊢ G \in TopGrp \to \underset{˙}{0} \in {Base}_{G}$
7	2 4	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
8		toponuni	$⊢ J \in TopOn ({Base}_{G}) \to {Base}_{G} = ⋃ J$
9	7 8	syl	$⊢ G \in TopGrp \to {Base}_{G} = ⋃ J$
10	6 9	eleqtrd	$⊢ G \in TopGrp \to \underset{˙}{0} \in ⋃ J$
11		eqid	$⊢ ⋃ J = ⋃ J$
12	11	sncld	$⊢ (J \in Haus \land \underset{˙}{0} \in ⋃ J) \to \{\underset{˙}{0}\} \in Clsd (J)$
13	12	expcom	$⊢ \underset{˙}{0} \in ⋃ J \to (J \in Haus \to \{\underset{˙}{0}\} \in Clsd (J))$
14	10 13	syl	$⊢ G \in TopGrp \to (J \in Haus \to \{\underset{˙}{0}\} \in Clsd (J))$
15		eqid	$⊢ -_{G} = -_{G}$
16	2 15	tgpsubcn	$⊢ G \in TopGrp \to -_{G} \in ((J \times_{t} J) Cn J)$
17		cnclima	$⊢ (-_{G} \in ((J \times_{t} J) Cn J) \land \{\underset{˙}{0}\} \in Clsd (J)) \to {-_{G}}^{-1} [\{\underset{˙}{0}\}] \in Clsd (J \times_{t} J)$
18	17	ex	$⊢ -_{G} \in ((J \times_{t} J) Cn J) \to (\{\underset{˙}{0}\} \in Clsd (J) \to {-_{G}}^{-1} [\{\underset{˙}{0}\}] \in Clsd (J \times_{t} J))$
19	16 18	syl	$⊢ G \in TopGrp \to (\{\underset{˙}{0}\} \in Clsd (J) \to {-_{G}}^{-1} [\{\underset{˙}{0}\}] \in Clsd (J \times_{t} J))$
20		cnvimass	$⊢ {-_{G}}^{-1} [\{\underset{˙}{0}\}] \subseteq dom -_{G}$
21	4 15	grpsubf	$⊢ G \in Grp \to -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G}$
22	3 21	syl	$⊢ G \in TopGrp \to -_{G} : {Base}_{G} \times {Base}_{G} ⟶ {Base}_{G}$
23	20 22	fssdm	$⊢ G \in TopGrp \to {-_{G}}^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{G} \times {Base}_{G}$
24		relxp	$⊢ Rel ({Base}_{G} \times {Base}_{G})$
25		relss	$⊢ {-_{G}}^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{G} \times {Base}_{G} \to (Rel ({Base}_{G} \times {Base}_{G}) \to Rel {-_{G}}^{-1} [\{\underset{˙}{0}\}])$
26	23 24 25	mpisyl	$⊢ G \in TopGrp \to Rel {-_{G}}^{-1} [\{\underset{˙}{0}\}]$
27		dfrel4v	$⊢ Rel {-_{G}}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow {-_{G}}^{-1} [\{\underset{˙}{0}\}] = \{⟨x, y⟩ \| x {-_{G}}^{-1} [\{\underset{˙}{0}\}] y\}$
28	26 27	sylib	$⊢ G \in TopGrp \to {-_{G}}^{-1} [\{\underset{˙}{0}\}] = \{⟨x, y⟩ \| x {-_{G}}^{-1} [\{\underset{˙}{0}\}] y\}$
29	22	ffnd	$⊢ G \in TopGrp \to -_{G} Fn ({Base}_{G} \times {Base}_{G})$
30		elpreima	$⊢ -_{G} Fn ({Base}_{G} \times {Base}_{G}) \to (⟨x, y⟩ \in {-_{G}}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\}))$
31	29 30	syl	$⊢ G \in TopGrp \to (⟨x, y⟩ \in {-_{G}}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\}))$
32		opelxp	$⊢ ⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \leftrightarrow (x \in {Base}_{G} \land y \in {Base}_{G})$
33	32	anbi1i	$⊢ (⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\}) \leftrightarrow ((x \in {Base}_{G} \land y \in {Base}_{G}) \land -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\})$
34	4 1 15	grpsubeq0	$⊢ (G \in Grp \land x \in {Base}_{G} \land y \in {Base}_{G}) \to (x -_{G} y = \underset{˙}{0} \leftrightarrow x = y)$
35	34	3expb	$⊢ (G \in Grp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (x -_{G} y = \underset{˙}{0} \leftrightarrow x = y)$
36	3 35	sylan	$⊢ (G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (x -_{G} y = \underset{˙}{0} \leftrightarrow x = y)$
37		df-ov	$⊢ x -_{G} y = -_{G} (⟨x, y⟩)$
38	37	eleq1i	$⊢ x -_{G} y \in \{\underset{˙}{0}\} \leftrightarrow -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\}$
39		ovex	$⊢ x -_{G} y \in V$
40	39	elsn	$⊢ x -_{G} y \in \{\underset{˙}{0}\} \leftrightarrow x -_{G} y = \underset{˙}{0}$
41	38 40	bitr3i	$⊢ -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\} \leftrightarrow x -_{G} y = \underset{˙}{0}$
42		equcom	$⊢ y = x \leftrightarrow x = y$
43	36 41 42	3bitr4g	$⊢ (G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (-_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\} \leftrightarrow y = x)$
44	43	pm5.32da	$⊢ G \in TopGrp \to (((x \in {Base}_{G} \land y \in {Base}_{G}) \land -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\}) \leftrightarrow ((x \in {Base}_{G} \land y \in {Base}_{G}) \land y = x))$
45	33 44	syl5bb	$⊢ G \in TopGrp \to ((⟨x, y⟩ \in ({Base}_{G} \times {Base}_{G}) \land -_{G} (⟨x, y⟩) \in \{\underset{˙}{0}\}) \leftrightarrow ((x \in {Base}_{G} \land y \in {Base}_{G}) \land y = x))$
46	31 45	bitrd	$⊢ G \in TopGrp \to (⟨x, y⟩ \in {-_{G}}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow ((x \in {Base}_{G} \land y \in {Base}_{G}) \land y = x))$
47		df-br	$⊢ x {-_{G}}^{-1} [\{\underset{˙}{0}\}] y \leftrightarrow ⟨x, y⟩ \in {-_{G}}^{-1} [\{\underset{˙}{0}\}]$
48		eleq1w	$⊢ y = x \to (y \in {Base}_{G} \leftrightarrow x \in {Base}_{G})$
49	48	biimparc	$⊢ (x \in {Base}_{G} \land y = x) \to y \in {Base}_{G}$
50	49	pm4.71i	$⊢ (x \in {Base}_{G} \land y = x) \leftrightarrow ((x \in {Base}_{G} \land y = x) \land y \in {Base}_{G})$
51		an32	$⊢ ((x \in {Base}_{G} \land y \in {Base}_{G}) \land y = x) \leftrightarrow ((x \in {Base}_{G} \land y = x) \land y \in {Base}_{G})$
52	50 51	bitr4i	$⊢ (x \in {Base}_{G} \land y = x) \leftrightarrow ((x \in {Base}_{G} \land y \in {Base}_{G}) \land y = x)$
53	46 47 52	3bitr4g	$⊢ G \in TopGrp \to (x {-_{G}}^{-1} [\{\underset{˙}{0}\}] y \leftrightarrow (x \in {Base}_{G} \land y = x))$
54	53	opabbidv	$⊢ G \in TopGrp \to \{⟨x, y⟩ \| x {-_{G}}^{-1} [\{\underset{˙}{0}\}] y\} = \{⟨x, y⟩ \| (x \in {Base}_{G} \land y = x)\}$
55		opabresid	$⊢ {I ↾}_{{Base}_{G}} = \{⟨x, y⟩ \| (x \in {Base}_{G} \land y = x)\}$
56	54 55	eqtr4di	$⊢ G \in TopGrp \to \{⟨x, y⟩ \| x {-_{G}}^{-1} [\{\underset{˙}{0}\}] y\} = {I ↾}_{{Base}_{G}}$
57	9	reseq2d	$⊢ G \in TopGrp \to {I ↾}_{{Base}_{G}} = {I ↾}_{⋃ J}$
58	28 56 57	3eqtrd	$⊢ G \in TopGrp \to {-_{G}}^{-1} [\{\underset{˙}{0}\}] = {I ↾}_{⋃ J}$
59	58	eleq1d	$⊢ G \in TopGrp \to ({-_{G}}^{-1} [\{\underset{˙}{0}\}] \in Clsd (J \times_{t} J) \leftrightarrow {I ↾}_{⋃ J} \in Clsd (J \times_{t} J))$
60	19 59	sylibd	$⊢ G \in TopGrp \to (\{\underset{˙}{0}\} \in Clsd (J) \to {I ↾}_{⋃ J} \in Clsd (J \times_{t} J))$
61		topontop	$⊢ J \in TopOn ({Base}_{G}) \to J \in Top$
62	7 61	syl	$⊢ G \in TopGrp \to J \in Top$
63	11	hausdiag	$⊢ J \in Haus \leftrightarrow (J \in Top \land {I ↾}_{⋃ J} \in Clsd (J \times_{t} J))$
64	63	baib	$⊢ J \in Top \to (J \in Haus \leftrightarrow {I ↾}_{⋃ J} \in Clsd (J \times_{t} J))$
65	62 64	syl	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow {I ↾}_{⋃ J} \in Clsd (J \times_{t} J))$
66	60 65	sylibrd	$⊢ G \in TopGrp \to (\{\underset{˙}{0}\} \in Clsd (J) \to J \in Haus)$
67	14 66	impbid	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow \{\underset{˙}{0}\} \in Clsd (J))$

Metamath Proof Explorer

Theorem tgphaus

Proof