tgpt0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgpt0		Structured version Visualization version GIF version

Theorem tgpt0 24276

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

**Hypothesis**
Ref	Expression
tgpt1.j	⊢ 𝐽 = (TopOpen‘𝐺)

**Assertion**
Ref	Expression
tgpt0	⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2))

Proof of Theorem tgpt0 Dummy variables 𝑤 𝑎 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgpt1.j	. . 3 ⊢ 𝐽 = (TopOpen‘𝐺)
2	1	tgpt1 24275	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre))
3		t1t0 23505	. . 3 ⊢ (𝐽 ∈ Fre → 𝐽 ∈ Kol2)
4		eleq2 2852	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧))
5		eleq2 2852	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑧))
6	4, 5	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
7	6	rspccva 3580	. . . . . . . . . 10 ⊢ ((∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
8	7	adantll 726	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
9		tgpgrp 24235	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
10	9	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝐺 ∈ Grp)
11		simpllr 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
12	11	simprd 500	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ (Base‘𝐺))
13		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐺) = (Base‘𝐺)
14		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
15		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (-_g‘𝐺) = (-_g‘𝐺)
16	13, 14, 15	grpsubid 19085	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑦(-_g‘𝐺)𝑦) = (0_g‘𝐺))
17	10, 12, 16	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑦(-_g‘𝐺)𝑦) = (0_g‘𝐺))
18	17	oveq1d 7425	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) = ((0_g‘𝐺)(+_g‘𝐺)𝑥))
19	11	simpld 499	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑥 ∈ (Base‘𝐺))
20		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
21	13, 20, 14	grplid 19029	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) → ((0_g‘𝐺)(+_g‘𝐺)𝑥) = 𝑥)
22	10, 19, 21	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((0_g‘𝐺)(+_g‘𝐺)𝑥) = 𝑥)
23	18, 22	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) = 𝑥)
24	13, 20, 15	grpnpcan 19093	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) = 𝑦)
25	10, 12, 19, 24	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) = 𝑦)
26		simprr 784	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ 𝑧)
27	25, 26	eqeltrd 2863	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) ∈ 𝑧)
28		oveq2 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑦(-_g‘𝐺)𝑎) = (𝑦(-_g‘𝐺)𝑥))
29	28	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) = ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥))
30	29	eleq1d 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) ∈ 𝑧 ↔ ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) ∈ 𝑧))
31		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) = (𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥))
32	31	mptpreima 6239	. . . . . . . . . . . . . . 15 ⊢ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) = {𝑎 ∈ (Base‘𝐺) ∣ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) ∈ 𝑧}
33	30, 32	elrab2 3654	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) ∈ 𝑧))
34	19, 27, 33	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧))
35		eleq2 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧)))
36		eleq2 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧)))
37	35, 36	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → ((𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) ↔ (𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧))))
38		simplr 780	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤))
39		tgptmd 24236	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
40	39	ad3antrrr 742	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝐺 ∈ TopMnd)
41	1, 13	tgptopon 24239	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
42	41	ad3antrrr 742	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
43	42, 42, 12	cnmptc 23819	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ 𝑦) ∈ (𝐽 Cn 𝐽))
44	42	cnmptid 23818	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ 𝑎) ∈ (𝐽 Cn 𝐽))
45	1, 15	tgpsubcn 24247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ TopGrp → (-_g‘𝐺) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽))
46	45	ad3antrrr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (-_g‘𝐺) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽))
47	42, 43, 44, 46	cnmpt12f 23823	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ (𝑦(-_g‘𝐺)𝑎)) ∈ (𝐽 Cn 𝐽))
48	42, 42, 19	cnmptc 23819	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ 𝑥) ∈ (𝐽 Cn 𝐽))
49	1, 20, 40, 42, 47, 48	cnmpt1plusg 24244	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) ∈ (𝐽 Cn 𝐽))
50		simprl 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
51		cnima 23422	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) ∈ (𝐽 Cn 𝐽) ∧ 𝑧 ∈ 𝐽) → (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ∈ 𝐽)
52	49, 50, 51	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ∈ 𝐽)
53	37, 38, 52	rspcdva 3582	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧)))
54	34, 53	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧))
55		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑦 → (𝑦(-_g‘𝐺)𝑎) = (𝑦(-_g‘𝐺)𝑦))
56	55	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑦 → ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) = ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥))
57	56	eleq1d 2848	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑦 → (((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) ∈ 𝑧 ↔ ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧))
58	57, 32	elrab2 3654	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ↔ (𝑦 ∈ (Base‘𝐺) ∧ ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧))
59	58	simprbi 502	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧)
60	54, 59	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧)
61	23, 60	eqeltrrd 2864	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
62	61	expr 461	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ 𝑧 ∈ 𝐽) → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
63	8, 62	impbid 215	. . . . . . . 8 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
64	63	ralrimiva 3157	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) → ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
65	64	ex 417	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)))
66	65	imim1d 83	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦) → (∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → 𝑥 = 𝑦)))
67	66	ralimdvva 3212	. . . 4 ⊢ (𝐺 ∈ TopGrp → (∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦) → ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → 𝑥 = 𝑦)))
68		ist0-2 23501	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)))
69	41, 68	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)))
70		ist1-2 23504	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → 𝑥 = 𝑦)))
71	41, 70	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → 𝑥 = 𝑦)))
72	67, 69, 71	3imtr4d 297	. . 3 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Kol2 → 𝐽 ∈ Fre))
73	3, 72	impbid2 229	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Fre ↔ 𝐽 ∈ Kol2))
74	2, 73	bitrd 282	1 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ∀wral 3079 ↦ cmpt 5192 ^◡ccnv 5660 “ cima 5664 ‘cfv 6536 (class class class)co 7410 Basecbs 17264 +_gcplusg 17305 TopOpenctopn 17469 0_gc0g 17487 Grpcgrp 18995 -_gcsg 18997 TopOnctopon 23067 Cn ccn 23381 Kol2ct0 23463 Frect1 23464 Hauscha 23465 ×_t ctx 23717 TopMndctmd 24227 TopGrpctgp 24228

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7982 df-2nd 7983 df-map 8822 df-0g 17489 df-topgen 17491 df-plusf 18692 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-grp 18998 df-minusg 18999 df-sbg 19000 df-top 23051 df-topon 23068 df-topsp 23090 df-bases 23103 df-cld 23176 df-cn 23384 df-cnp 23385 df-t0 23470 df-t1 23471 df-haus 23472 df-tx 23719 df-tmd 24229 df-tgp 24230

This theorem is referenced by: (None)

W3C validator