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 24493

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 24492	. 2 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre))
3		t1t0 23721	. . 3 ⊢ (𝐽 ∈ Fre → 𝐽 ∈ Kol2)
4		eleq2 2853	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧))
5		eleq2 2853	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑧))
6	4, 5	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → ((𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
7	6	rspccva 3579	. . . . . . . . . 10 ⊢ ((∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
8	7	adantll 727	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
9		tgpgrp 24452	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
10	9	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝐺 ∈ Grp)
11		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))
12	11	simprd 501	. . . . . . . . . . . . . 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 19284	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑦(-_g‘𝐺)𝑦) = (0_g‘𝐺))
17	10, 12, 16	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑦(-_g‘𝐺)𝑦) = (0_g‘𝐺))
18	17	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) = ((0_g‘𝐺)(+_g‘𝐺)𝑥))
19	11	simpld 500	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑥 ∈ (Base‘𝐺))
20		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
21	13, 20, 14	grplid 19228	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) → ((0_g‘𝐺)(+_g‘𝐺)𝑥) = 𝑥)
22	10, 19, 21	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((0_g‘𝐺)(+_g‘𝐺)𝑥) = 𝑥)
23	18, 22	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) = 𝑥)
24	13, 20, 15	grpnpcan 19292	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) = 𝑦)
25	10, 12, 19, 24	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) = 𝑦)
26		simprr 785	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ 𝑧)
27	25, 26	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) ∈ 𝑧)
28		oveq2 7459	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑦(-_g‘𝐺)𝑎) = (𝑦(-_g‘𝐺)𝑥))
29	28	oveq1d 7466	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) = ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥))
30	29	eleq1d 2849	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) ∈ 𝑧 ↔ ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) ∈ 𝑧))
31		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) = (𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥))
32	31	mptpreima 6258	. . . . . . . . . . . . . . 15 ⊢ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) = {𝑎 ∈ (Base‘𝐺) ∣ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) ∈ 𝑧}
33	30, 32	elrab2 3652	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ↔ (𝑥 ∈ (Base‘𝐺) ∧ ((𝑦(-_g‘𝐺)𝑥)(+_g‘𝐺)𝑥) ∈ 𝑧))
34	19, 27, 33	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧))
35		eleq2 2853	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧)))
36		eleq2 2853	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧)))
37	35, 36	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → ((𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) ↔ (𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧))))
38		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤))
39		tgptmd 24453	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
40	39	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝐺 ∈ TopMnd)
41	1, 13	tgptopon 24456	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
42	41	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
43	42, 42, 12	cnmptc 24036	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ 𝑦) ∈ (𝐽 Cn 𝐽))
44	42	cnmptid 24035	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ 𝑎) ∈ (𝐽 Cn 𝐽))
45	1, 15	tgpsubcn 24464	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ TopGrp → (-_g‘𝐺) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽))
46	45	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (-_g‘𝐺) ∈ ((𝐽 ×_t 𝐽) Cn 𝐽))
47	42, 43, 44, 46	cnmpt12f 24040	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ (𝑦(-_g‘𝐺)𝑎)) ∈ (𝐽 Cn 𝐽))
48	42, 42, 19	cnmptc 24036	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ 𝑥) ∈ (𝐽 Cn 𝐽))
49	1, 20, 40, 42, 47, 48	cnmpt1plusg 24461	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) ∈ (𝐽 Cn 𝐽))
50		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
51		cnima 23638	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) ∈ (𝐽 Cn 𝐽) ∧ 𝑧 ∈ 𝐽) → (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ∈ 𝐽)
52	49, 50, 51	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ∈ 𝐽)
53	37, 38, 52	rspcdva 3581	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → (𝑥 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧)))
54	34, 53	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧))
55		oveq2 7459	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑦 → (𝑦(-_g‘𝐺)𝑎) = (𝑦(-_g‘𝐺)𝑦))
56	55	oveq1d 7466	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑦 → ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) = ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥))
57	56	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑦 → (((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥) ∈ 𝑧 ↔ ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧))
58	57, 32	elrab2 3652	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) ↔ (𝑦 ∈ (Base‘𝐺) ∧ ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧))
59	58	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (^◡(𝑎 ∈ (Base‘𝐺) ↦ ((𝑦(-_g‘𝐺)𝑎)(+_g‘𝐺)𝑥)) “ 𝑧) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧)
60	54, 59	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → ((𝑦(-_g‘𝐺)𝑦)(+_g‘𝐺)𝑥) ∈ 𝑧)
61	23, 60	eqeltrrd 2865	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ (𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧)) → 𝑥 ∈ 𝑧)
62	61	expr 462	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ 𝑧 ∈ 𝐽) → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
63	8, 62	impbid 215	. . . . . . . 8 ⊢ ((((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
64	63	ralrimiva 3158	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ ∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)) → ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
65	64	ex 418	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)))
66	65	imim1d 83	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦) → (∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → 𝑥 = 𝑦)))
67	66	ralimdvva 3213	. . . 4 ⊢ (𝐺 ∈ TopGrp → (∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦) → ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑤 ∈ 𝐽 (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤) → 𝑥 = 𝑦)))
68		ist0-2 23717	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)))
69	41, 68	syl 18	. . . 4 ⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)))
70		ist1-2 23720	. . . . 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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 ↦ cmpt 5192 ^◡ccnv 5657 “ cima 5661 ‘cfv 6566 (class class class)co 7451 Basecbs 17431 +_gcplusg 17472 TopOpenctopn 17642 0_gc0g 17660 Grpcgrp 19194 -_gcsg 19196 TopOnctopon 23283 Cn ccn 23597 Kol2ct0 23679 Frect1 23680 Hauscha 23681 ×_t ctx 23934 TopMndctmd 24444 TopGrpctgp 24445

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-id 5553 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-1st 8035 df-2nd 8036 df-map 8887 df-0g 17662 df-topgen 17664 df-plusf 18865 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-grp 19197 df-minusg 19198 df-sbg 19199 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-cn 23600 df-cnp 23601 df-t0 23686 df-t1 23687 df-haus 23688 df-tx 23936 df-tmd 24446 df-tgp 24447

This theorem is used by: (None)

W3C validator