Step | Hyp | Ref
| Expression |
1 | | tgpgrp 21882 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
3 | | tgphaus.1 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
4 | 2, 3 | grpidcl 17450 |
. . . . 5
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝐺 ∈ TopGrp → 0 ∈
(Base‘𝐺)) |
6 | | tgphaus.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝐺) |
7 | 6, 2 | tgptopon 21886 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈
(TopOn‘(Base‘𝐺))) |
8 | | toponuni 20719 |
. . . . 5
⊢ (𝐽 ∈
(TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝐺 ∈ TopGrp →
(Base‘𝐺) = ∪ 𝐽) |
10 | 5, 9 | eleqtrd 2703 |
. . 3
⊢ (𝐺 ∈ TopGrp → 0 ∈ ∪ 𝐽) |
11 | | eqid 2622 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
12 | 11 | sncld 21175 |
. . . 4
⊢ ((𝐽 ∈ Haus ∧ 0 ∈ ∪ 𝐽)
→ { 0 } ∈ (Clsd‘𝐽)) |
13 | 12 | expcom 451 |
. . 3
⊢ ( 0 ∈ ∪ 𝐽
→ (𝐽 ∈ Haus
→ { 0 } ∈ (Clsd‘𝐽))) |
14 | 10, 13 | syl 17 |
. 2
⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus → { 0 } ∈
(Clsd‘𝐽))) |
15 | | eqid 2622 |
. . . . . 6
⊢
(-g‘𝐺) = (-g‘𝐺) |
16 | 6, 15 | tgpsubcn 21894 |
. . . . 5
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
17 | | cnclima 21072 |
. . . . . 6
⊢
(((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ { 0 } ∈ (Clsd‘𝐽)) → (◡(-g‘𝐺) “ { 0 }) ∈
(Clsd‘(𝐽
×t 𝐽))) |
18 | 17 | ex 450 |
. . . . 5
⊢
((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) → ({ 0 } ∈ (Clsd‘𝐽) → (◡(-g‘𝐺) “ { 0 }) ∈
(Clsd‘(𝐽
×t 𝐽)))) |
19 | 16, 18 | syl 17 |
. . . 4
⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈
(Clsd‘𝐽) →
(◡(-g‘𝐺) “ { 0 }) ∈
(Clsd‘(𝐽
×t 𝐽)))) |
20 | | cnvimass 5485 |
. . . . . . . . 9
⊢ (◡(-g‘𝐺) “ { 0 }) ⊆ dom
(-g‘𝐺) |
21 | 2, 15 | grpsubf 17494 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
22 | 1, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
23 | | fdm 6051 |
. . . . . . . . . 10
⊢
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → dom (-g‘𝐺) = ((Base‘𝐺) × (Base‘𝐺))) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopGrp → dom
(-g‘𝐺) =
((Base‘𝐺) ×
(Base‘𝐺))) |
25 | 20, 24 | syl5sseq 3653 |
. . . . . . . 8
⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) ⊆
((Base‘𝐺) ×
(Base‘𝐺))) |
26 | | relxp 5227 |
. . . . . . . 8
⊢ Rel
((Base‘𝐺) ×
(Base‘𝐺)) |
27 | | relss 5206 |
. . . . . . . 8
⊢ ((◡(-g‘𝐺) “ { 0 }) ⊆
((Base‘𝐺) ×
(Base‘𝐺)) → (Rel
((Base‘𝐺) ×
(Base‘𝐺)) → Rel
(◡(-g‘𝐺) “ { 0 }))) |
28 | 25, 26, 27 | mpisyl 21 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp → Rel (◡(-g‘𝐺) “ { 0 })) |
29 | | dfrel4v 5584 |
. . . . . . 7
⊢ (Rel
(◡(-g‘𝐺) “ { 0 }) ↔ (◡(-g‘𝐺) “ { 0 }) = {〈𝑥, 𝑦〉 ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦}) |
30 | 28, 29 | sylib 208 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = {〈𝑥, 𝑦〉 ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦}) |
31 | | ffn 6045 |
. . . . . . . . . . . 12
⊢
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺))) |
32 | 22, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺) Fn
((Base‘𝐺) ×
(Base‘𝐺))) |
33 | | elpreima 6337 |
. . . . . . . . . . 11
⊢
((-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 }))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp →
(〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ { 0 }) ↔ (〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 }))) |
35 | | opelxp 5146 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) |
36 | 35 | anbi1i 731 |
. . . . . . . . . . 11
⊢
((〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧
((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 })) |
37 | 2, 3, 15 | grpsubeq0 17501 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦)) |
38 | 37 | 3expb 1266 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦)) |
39 | 1, 38 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦) = 0 ↔ 𝑥 = 𝑦)) |
40 | | df-ov 6653 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘〈𝑥, 𝑦〉) |
41 | 40 | eleq1i 2692 |
. . . . . . . . . . . . . 14
⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔
((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 }) |
42 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(-g‘𝐺)𝑦) ∈ V |
43 | 42 | elsn 4192 |
. . . . . . . . . . . . . 14
⊢ ((𝑥(-g‘𝐺)𝑦) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 ) |
44 | 41, 43 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢
(((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 } ↔ (𝑥(-g‘𝐺)𝑦) = 0 ) |
45 | | equcom 1945 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) |
46 | 39, 44, 45 | 3bitr4g 303 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 } ↔ 𝑦 = 𝑥)) |
47 | 46 | pm5.32da 673 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ TopGrp → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))) |
48 | 36, 47 | syl5bb 272 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopGrp →
((〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧
((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))) |
49 | 34, 48 | bitrd 268 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopGrp →
(〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ { 0 }) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥))) |
50 | | df-br 4654 |
. . . . . . . . 9
⊢ (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ { 0 })) |
51 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦 ∈ (Base‘𝐺) ↔ 𝑥 ∈ (Base‘𝐺))) |
52 | 51 | biimparc 504 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) → 𝑦 ∈ (Base‘𝐺)) |
53 | 52 | pm4.71i 664 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺))) |
54 | | an32 839 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ∧ 𝑦 ∈ (Base‘𝐺))) |
55 | 53, 54 | bitr4i 267 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑦 = 𝑥)) |
56 | 49, 50, 55 | 3bitr4g 303 |
. . . . . . . 8
⊢ (𝐺 ∈ TopGrp → (𝑥(◡(-g‘𝐺) “ { 0 })𝑦 ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥))) |
57 | 56 | opabbidv 4716 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp →
{〈𝑥, 𝑦〉 ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)}) |
58 | | opabresid 5455 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 = 𝑥)} = ( I ↾ (Base‘𝐺)) |
59 | 57, 58 | syl6eq 2672 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp →
{〈𝑥, 𝑦〉 ∣ 𝑥(◡(-g‘𝐺) “ { 0 })𝑦} = ( I ↾ (Base‘𝐺))) |
60 | 9 | reseq2d 5396 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → ( I
↾ (Base‘𝐺)) = (
I ↾ ∪ 𝐽)) |
61 | 30, 59, 60 | 3eqtrd 2660 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → (◡(-g‘𝐺) “ { 0 }) = ( I ↾ ∪ 𝐽)) |
62 | 61 | eleq1d 2686 |
. . . 4
⊢ (𝐺 ∈ TopGrp → ((◡(-g‘𝐺) “ { 0 }) ∈
(Clsd‘(𝐽
×t 𝐽))
↔ ( I ↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
63 | 19, 62 | sylibd 229 |
. . 3
⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈
(Clsd‘𝐽) → ( I
↾ ∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
64 | | topontop 20718 |
. . . . 5
⊢ (𝐽 ∈
(TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top) |
65 | 7, 64 | syl 17 |
. . . 4
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ Top) |
66 | 11 | hausdiag 21448 |
. . . . 5
⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾
∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
67 | 66 | baib 944 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐽 ∈ Haus ↔ ( I ↾
∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
68 | 65, 67 | syl 17 |
. . 3
⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ ( I ↾
∪ 𝐽) ∈ (Clsd‘(𝐽 ×t 𝐽)))) |
69 | 63, 68 | sylibrd 249 |
. 2
⊢ (𝐺 ∈ TopGrp → ({ 0 } ∈
(Clsd‘𝐽) → 𝐽 ∈ Haus)) |
70 | 14, 69 | impbid 202 |
1
⊢ (𝐺 ∈ TopGrp → (𝐽 ∈ Haus ↔ { 0 } ∈
(Clsd‘𝐽))) |