tgpt0

Description: Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015)

		Ref	Expression
	Hypothesis	tgpt1.j	$⊢ J = TopOpen (G)$
	Assertion	tgpt0	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow J \in Kol2)$

Proof

Step	Hyp	Ref	Expression
1		tgpt1.j	$⊢ J = TopOpen (G)$
2	1	tgpt1	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow J \in Fre)$
3		t1t0	$⊢ J \in Fre \to J \in Kol2$
4		eleq2	$⊢ w = z \to (x \in w \leftrightarrow x \in z)$
5		eleq2	$⊢ w = z \to (y \in w \leftrightarrow y \in z)$
6	4 5	imbi12d	$⊢ w = z \to ((x \in w \to y \in w) \leftrightarrow (x \in z \to y \in z))$
7	6	rspccva	$⊢ (\forall w \in J (x \in w \to y \in w) \land z \in J) \to (x \in z \to y \in z)$
8	7	adantll	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land z \in J) \to (x \in z \to y \in z)$
9		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
10	9	ad3antrrr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to G \in Grp$
11		simpllr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (x \in {Base}_{G} \land y \in {Base}_{G})$
12	11	simprd	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to y \in {Base}_{G}$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14		eqid	$⊢ 0_{G} = 0_{G}$
15		eqid	$⊢ -_{G} = -_{G}$
16	13 14 15	grpsubid	$⊢ (G \in Grp \land y \in {Base}_{G}) \to y -_{G} y = 0_{G}$
17	10 12 16	syl2anc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to y -_{G} y = 0_{G}$
18	17	oveq1d	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (y -_{G} y) +_{G} x = 0_{G} +_{G} x$
19	11	simpld	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to x \in {Base}_{G}$
20		eqid	$⊢ +_{G} = +_{G}$
21	13 20 14	grplid	$⊢ (G \in Grp \land x \in {Base}_{G}) \to 0_{G} +_{G} x = x$
22	10 19 21	syl2anc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to 0_{G} +_{G} x = x$
23	18 22	eqtrd	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (y -_{G} y) +_{G} x = x$
24	13 20 15	grpnpcan	$⊢ (G \in Grp \land y \in {Base}_{G} \land x \in {Base}_{G}) \to (y -_{G} x) +_{G} x = y$
25	10 12 19 24	syl3anc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (y -_{G} x) +_{G} x = y$
26		simprr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to y \in z$
27	25 26	eqeltrd	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (y -_{G} x) +_{G} x \in z$
28		oveq2	$⊢ a = x \to y -_{G} a = y -_{G} x$
29	28	oveq1d	$⊢ a = x \to (y -_{G} a) +_{G} x = (y -_{G} x) +_{G} x$
30	29	eleq1d	$⊢ a = x \to ((y -_{G} a) +_{G} x \in z \leftrightarrow (y -_{G} x) +_{G} x \in z)$
31		eqid	$⊢ (a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x) = (a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)$
32	31	mptpreima	$⊢ {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] = \{a \in {Base}_{G} \| (y -_{G} a) +_{G} x \in z\}$
33	30 32	elrab2	$⊢ x \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \leftrightarrow (x \in {Base}_{G} \land (y -_{G} x) +_{G} x \in z)$
34	19 27 33	sylanbrc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to x \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z]$
35		eleq2	$⊢ w = {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \to (x \in w \leftrightarrow x \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z])$
36		eleq2	$⊢ w = {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \to (y \in w \leftrightarrow y \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z])$
37	35 36	imbi12d	$⊢ w = {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \to ((x \in w \to y \in w) \leftrightarrow (x \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \to y \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z]))$
38		simplr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to \forall w \in J (x \in w \to y \in w)$
39		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
40	39	ad3antrrr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to G \in TopMnd$
41	1 13	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
42	41	ad3antrrr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to J \in TopOn ({Base}_{G})$
43	42 42 12	cnmptc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (a \in {Base}_{G} ⟼ y) \in (J Cn J)$
44	42	cnmptid	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (a \in {Base}_{G} ⟼ a) \in (J Cn J)$
45	1 15	tgpsubcn	$⊢ G \in TopGrp \to -_{G} \in ((J \times_{t} J) Cn J)$
46	45	ad3antrrr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to -_{G} \in ((J \times_{t} J) Cn J)$
47	42 43 44 46	cnmpt12f	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (a \in {Base}_{G} ⟼ y -_{G} a) \in (J Cn J)$
48	42 42 19	cnmptc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (a \in {Base}_{G} ⟼ x) \in (J Cn J)$
49	1 20 40 42 47 48	cnmpt1plusg	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x) \in (J Cn J)$
50		simprl	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to z \in J$
51		cnima	$⊢ ((a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x) \in (J Cn J) \land z \in J) \to {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \in J$
52	49 50 51	syl2anc	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \in J$
53	37 38 52	rspcdva	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (x \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \to y \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z])$
54	34 53	mpd	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to y \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z]$
55		oveq2	$⊢ a = y \to y -_{G} a = y -_{G} y$
56	55	oveq1d	$⊢ a = y \to (y -_{G} a) +_{G} x = (y -_{G} y) +_{G} x$
57	56	eleq1d	$⊢ a = y \to ((y -_{G} a) +_{G} x \in z \leftrightarrow (y -_{G} y) +_{G} x \in z)$
58	57 32	elrab2	$⊢ y \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \leftrightarrow (y \in {Base}_{G} \land (y -_{G} y) +_{G} x \in z)$
59	58	simprbi	$⊢ y \in {(a \in {Base}_{G} ⟼ (y -_{G} a) +_{G} x)}^{-1} [z] \to (y -_{G} y) +_{G} x \in z$
60	54 59	syl	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to (y -_{G} y) +_{G} x \in z$
61	23 60	eqeltrrd	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land (z \in J \land y \in z)) \to x \in z$
62	61	expr	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land z \in J) \to (y \in z \to x \in z)$
63	8 62	impbid	$⊢ (((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \land z \in J) \to (x \in z \leftrightarrow y \in z)$
64	63	ralrimiva	$⊢ ((G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \land \forall w \in J (x \in w \to y \in w)) \to \forall z \in J (x \in z \leftrightarrow y \in z)$
65	64	ex	$⊢ (G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (\forall w \in J (x \in w \to y \in w) \to \forall z \in J (x \in z \leftrightarrow y \in z))$
66	65	imim1d	$⊢ (G \in TopGrp \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to ((\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y) \to (\forall w \in J (x \in w \to y \in w) \to x = y))$
67	66	ralimdvva	$⊢ G \in TopGrp \to (\forall x \in {Base}_{G} \forall y \in {Base}_{G} (\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y) \to \forall x \in {Base}_{G} \forall y \in {Base}_{G} (\forall w \in J (x \in w \to y \in w) \to x = y))$
68		ist0-2	$⊢ J \in TopOn ({Base}_{G}) \to (J \in Kol2 \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} (\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y))$
69	41 68	syl	$⊢ G \in TopGrp \to (J \in Kol2 \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} (\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y))$
70		ist1-2	$⊢ J \in TopOn ({Base}_{G}) \to (J \in Fre \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} (\forall w \in J (x \in w \to y \in w) \to x = y))$
71	41 70	syl	$⊢ G \in TopGrp \to (J \in Fre \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} (\forall w \in J (x \in w \to y \in w) \to x = y))$
72	67 69 71	3imtr4d	$⊢ G \in TopGrp \to (J \in Kol2 \to J \in Fre)$
73	3 72	impbid2	$⊢ G \in TopGrp \to (J \in Fre \leftrightarrow J \in Kol2)$
74	2 73	bitrd	$⊢ G \in TopGrp \to (J \in Haus \leftrightarrow J \in Kol2)$

Metamath Proof Explorer

Theorem tgpt0

Proof