Metamath Proof Explorer

Theorem tgpt0

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

Ref Expression
Hypothesis tgpt1.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion tgpt0 ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2 ) )

Proof

Step Hyp Ref Expression
1 tgpt1.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 1 tgpt1 ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Fre ) )
3 t1t0 ⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )
4 eleq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧 ) )
5 eleq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑧 ) )
6 4 5 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ↔ ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
7 6 rspccva ⊢ ( ( ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )
8 7 adantll ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )
9 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
10 9 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝐺 ∈ Grp )
11 simpllr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) )
12 11 simprd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
13 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
15 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
16 13 14 15 grpsubid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
17 10 12 16 syl2anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
18 17 oveq1d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) )
19 11 simpld ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
20 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
21 13 20 14 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
22 10 19 21 syl2anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
23 18 22 eqtrd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
24 13 20 15 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 )
25 10 12 19 24 syl3anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 )
26 simprr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑦 ∈ 𝑧 )
27 25 26 eqeltrd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 )
28 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) = ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) )
29 28 oveq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) 𝑥 ) )
30 29 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ) )
31 eqid ⊢ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) )
32 31 mptpreima ⊢ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) = { 𝑎 ∈ ( Base ‘ 𝐺 ) ∣ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 }
33 30 32 elrab2 ⊢ ( 𝑥 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑥 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ) )
34 19 27 33 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑥 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) )
35 eleq2 ⊢ ( 𝑤 = ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ) )
36 eleq2 ⊢ ( 𝑤 = ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ) )
37 35 36 imbi12d ⊢ ( 𝑤 = ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) → ( ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ↔ ( 𝑥 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) → 𝑦 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ) ) )
38 simplr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) )
39 tgptmd ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
40 39 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝐺 ∈ TopMnd )
41 1 13 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
42 41 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
43 42 42 12 cnmptc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
44 42 cnmptid ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ 𝑎 ) ∈ ( 𝐽 Cn 𝐽 ) )
45 1 15 tgpsubcn ⊢ ( 𝐺 ∈ TopGrp → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
46 45 ad3antrrr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
47 42 43 44 46 cnmpt12f ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
48 42 42 19 cnmptc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
49 1 20 40 42 47 48 cnmpt1plusg ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
50 simprl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑧 ∈ 𝐽 )
51 cnima ⊢ ( ( ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) → ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ∈ 𝐽 )
52 49 50 51 syl2anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ∈ 𝐽 )
53 37 38 52 rspcdva ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑥 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) → 𝑦 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ) )
54 34 53 mpd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑦 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) )
55 oveq2 ⊢ ( 𝑎 = 𝑦 → ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) = ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) )
56 55 oveq1d ⊢ ( 𝑎 = 𝑦 → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) )
57 56 eleq1d ⊢ ( 𝑎 = 𝑦 → ( ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ) )
58 57 32 elrab2 ⊢ ( 𝑦 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ) )
59 58 simprbi ⊢ ( 𝑦 ∈ ( ◡ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑎 ) ( +g ‘ 𝐺 ) 𝑥 ) ) “ 𝑧 ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 )
60 54 59 syl ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → ( ( 𝑦 ( -g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 )
61 23 60 eqeltrrd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑦 ∈ 𝑧 ) ) → 𝑥 ∈ 𝑧 )
62 61 expr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧 ) )
63 8 62 impbid ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
64 63 ralrimiva ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) → ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
65 64 ex ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) → ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) ) )
66 65 imim1d ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) → ( ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) → 𝑥 = 𝑦 ) ) )
67 66 ralimdvva ⊢ ( 𝐺 ∈ TopGrp → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) → 𝑥 = 𝑦 ) ) )
68 ist0-2 ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) )
69 41 68 syl ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) )
70 ist1-2 ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) → 𝑥 = 𝑦 ) ) )
71 41 70 syl ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ∀ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) → 𝑥 = 𝑦 ) ) )
72 67 69 71 3imtr4d ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Kol2 → 𝐽 ∈ Fre ) )
73 3 72 impbid2 ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Fre ↔ 𝐽 ∈ Kol2 ) )
74 2 73 bitrd ⊢ ( 𝐺 ∈ TopGrp → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2 ) )