Step | Hyp | Ref
| Expression |
1 | | ngpgrp 22213 |
. . 3
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) → 𝐺 ∈ Grp) |
3 | | ngpms 22214 |
. . . 4
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) |
4 | 3 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) → 𝐺 ∈ MetSp) |
5 | | mstps 22070 |
. . 3
⊢ (𝐺 ∈ MetSp → 𝐺 ∈ TopSp) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) → 𝐺 ∈ TopSp) |
7 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
8 | | eqid 2610 |
. . . . . 6
⊢
(-g‘𝐺) = (-g‘𝐺) |
9 | 7, 8 | grpsubf 17317 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
10 | 2, 9 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
(-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
11 | | rphalfcl 11734 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ+
→ (𝑧 / 2) ∈
ℝ+) |
12 | 11 | adantl 481 |
. . . . . . 7
⊢ ((((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) ∈
ℝ+) |
13 | | simplll 794 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel)) |
14 | 13, 4 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝐺 ∈ MetSp) |
15 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) |
16 | 15 | simpld 474 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝑥 ∈ (Base‘𝐺)) |
17 | | simprl 790 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝑢 ∈ (Base‘𝐺)) |
18 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(dist‘𝐺) =
(dist‘𝐺) |
19 | 7, 18 | mscl 22076 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ MetSp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺)) → (𝑥(dist‘𝐺)𝑢) ∈ ℝ) |
20 | 14, 16, 17, 19 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑥(dist‘𝐺)𝑢) ∈ ℝ) |
21 | 15 | simprd 478 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺)) |
22 | | simprr 792 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝑣 ∈ (Base‘𝐺)) |
23 | 7, 18 | mscl 22076 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ MetSp ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺)) → (𝑦(dist‘𝐺)𝑣) ∈ ℝ) |
24 | 14, 21, 22, 23 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑦(dist‘𝐺)𝑣) ∈ ℝ) |
25 | | rpre 11715 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
26 | 25 | ad2antlr 759 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝑧 ∈ ℝ) |
27 | | lt2halves 11144 |
. . . . . . . . . . 11
⊢ (((𝑥(dist‘𝐺)𝑢) ∈ ℝ ∧ (𝑦(dist‘𝐺)𝑣) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑥(dist‘𝐺)𝑢) < (𝑧 / 2) ∧ (𝑦(dist‘𝐺)𝑣) < (𝑧 / 2)) → ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) < 𝑧)) |
28 | 20, 24, 26, 27 | syl3anc 1318 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥(dist‘𝐺)𝑢) < (𝑧 / 2) ∧ (𝑦(dist‘𝐺)𝑣) < (𝑧 / 2)) → ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) < 𝑧)) |
29 | 13, 2 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝐺 ∈ Grp) |
30 | 7, 8 | grpsubcl 17318 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(-g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
31 | 29, 16, 21, 30 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑥(-g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
32 | 7, 8 | grpsubcl 17318 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺)) → (𝑢(-g‘𝐺)𝑣) ∈ (Base‘𝐺)) |
33 | 29, 17, 22, 32 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑢(-g‘𝐺)𝑣) ∈ (Base‘𝐺)) |
34 | 7, 8 | grpsubcl 17318 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑢(-g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
35 | 29, 17, 21, 34 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑢(-g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
36 | 7, 18 | mstri 22084 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ MetSp ∧ ((𝑥(-g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ (𝑢(-g‘𝐺)𝑣) ∈ (Base‘𝐺) ∧ (𝑢(-g‘𝐺)𝑦) ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ≤ (((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑦)) + ((𝑢(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)))) |
37 | 14, 31, 33, 35, 36 | syl13anc 1320 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ≤ (((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑦)) + ((𝑢(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)))) |
38 | 13 | simpld 474 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → 𝐺 ∈ NrmGrp) |
39 | 7, 8, 18 | ngpsubcan 22228 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ NrmGrp ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑦)) = (𝑥(dist‘𝐺)𝑢)) |
40 | 38, 16, 17, 21, 39 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑦)) = (𝑥(dist‘𝐺)𝑢)) |
41 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐺) = (+g‘𝐺) |
42 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝐺) = (invg‘𝐺) |
43 | 7, 41, 42, 8 | grpsubval 17288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑢(-g‘𝐺)𝑦) = (𝑢(+g‘𝐺)((invg‘𝐺)‘𝑦))) |
44 | 17, 21, 43 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑢(-g‘𝐺)𝑦) = (𝑢(+g‘𝐺)((invg‘𝐺)‘𝑦))) |
45 | 7, 41, 42, 8 | grpsubval 17288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺)) → (𝑢(-g‘𝐺)𝑣) = (𝑢(+g‘𝐺)((invg‘𝐺)‘𝑣))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑢(-g‘𝐺)𝑣) = (𝑢(+g‘𝐺)((invg‘𝐺)‘𝑣))) |
47 | 44, 46 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑢(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) = ((𝑢(+g‘𝐺)((invg‘𝐺)‘𝑦))(dist‘𝐺)(𝑢(+g‘𝐺)((invg‘𝐺)‘𝑣)))) |
48 | 7, 42 | grpinvcl 17290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑦) ∈ (Base‘𝐺)) |
49 | 29, 21, 48 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((invg‘𝐺)‘𝑦) ∈ (Base‘𝐺)) |
50 | 7, 42 | grpinvcl 17290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝑣 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑣) ∈ (Base‘𝐺)) |
51 | 29, 22, 50 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((invg‘𝐺)‘𝑣) ∈ (Base‘𝐺)) |
52 | 7, 41, 18 | ngplcan 22225 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧
(((invg‘𝐺)‘𝑦) ∈ (Base‘𝐺) ∧ ((invg‘𝐺)‘𝑣) ∈ (Base‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)((invg‘𝐺)‘𝑦))(dist‘𝐺)(𝑢(+g‘𝐺)((invg‘𝐺)‘𝑣))) = (((invg‘𝐺)‘𝑦)(dist‘𝐺)((invg‘𝐺)‘𝑣))) |
53 | 13, 49, 51, 17, 52 | syl13anc 1320 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑢(+g‘𝐺)((invg‘𝐺)‘𝑦))(dist‘𝐺)(𝑢(+g‘𝐺)((invg‘𝐺)‘𝑣))) = (((invg‘𝐺)‘𝑦)(dist‘𝐺)((invg‘𝐺)‘𝑣))) |
54 | 7, 42, 18 | ngpinvds 22227 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((invg‘𝐺)‘𝑦)(dist‘𝐺)((invg‘𝐺)‘𝑣)) = (𝑦(dist‘𝐺)𝑣)) |
55 | 13, 21, 22, 54 | syl12anc 1316 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((invg‘𝐺)‘𝑦)(dist‘𝐺)((invg‘𝐺)‘𝑣)) = (𝑦(dist‘𝐺)𝑣)) |
56 | 47, 53, 55 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑢(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) = (𝑦(dist‘𝐺)𝑣)) |
57 | 40, 56 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑦)) + ((𝑢(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣))) = ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣))) |
58 | 37, 57 | breqtrd 4609 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ≤ ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣))) |
59 | 7, 18 | mscl 22076 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ MetSp ∧ (𝑥(-g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ (𝑢(-g‘𝐺)𝑣) ∈ (Base‘𝐺)) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ∈ ℝ) |
60 | 14, 31, 33, 59 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ∈ ℝ) |
61 | 20, 24 | readdcld 9948 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) ∈ ℝ) |
62 | | lelttr 10007 |
. . . . . . . . . . . 12
⊢ ((((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ∈ ℝ ∧ ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ≤ ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) ∧ ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) < 𝑧) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
63 | 60, 61, 26, 62 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) ≤ ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) ∧ ((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) < 𝑧) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
64 | 58, 63 | mpand 707 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥(dist‘𝐺)𝑢) + (𝑦(dist‘𝐺)𝑣)) < 𝑧 → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
65 | 28, 64 | syld 46 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥(dist‘𝐺)𝑢) < (𝑧 / 2) ∧ (𝑦(dist‘𝐺)𝑣) < (𝑧 / 2)) → ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
66 | 16, 17 | ovresd 6699 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) = (𝑥(dist‘𝐺)𝑢)) |
67 | 66 | breq1d 4593 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ↔ (𝑥(dist‘𝐺)𝑢) < (𝑧 / 2))) |
68 | 21, 22 | ovresd 6699 |
. . . . . . . . . . 11
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) = (𝑦(dist‘𝐺)𝑣)) |
69 | 68 | breq1d 4593 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2) ↔ (𝑦(dist‘𝐺)𝑣) < (𝑧 / 2))) |
70 | 67, 69 | anbi12d 743 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)) ↔ ((𝑥(dist‘𝐺)𝑢) < (𝑧 / 2) ∧ (𝑦(dist‘𝐺)𝑣) < (𝑧 / 2)))) |
71 | 31, 33 | ovresd 6699 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) = ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣))) |
72 | 71 | breq1d 4593 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧 ↔ ((𝑥(-g‘𝐺)𝑦)(dist‘𝐺)(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
73 | 65, 70, 72 | 3imtr4d 282 |
. . . . . . . 8
⊢
(((((𝐺 ∈ NrmGrp
∧ 𝐺 ∈ Abel) ∧
(𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) ∧ (𝑢 ∈ (Base‘𝐺) ∧ 𝑣 ∈ (Base‘𝐺))) → (((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
74 | 73 | ralrimivva 2954 |
. . . . . . 7
⊢ ((((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) →
∀𝑢 ∈
(Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
75 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑧 / 2) → ((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ↔ (𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2))) |
76 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑧 / 2) → ((𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟 ↔ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2))) |
77 | 75, 76 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑧 / 2) → (((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) ↔ ((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)))) |
78 | 77 | imbi1d 330 |
. . . . . . . . 9
⊢ (𝑟 = (𝑧 / 2) → ((((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧) ↔ (((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧))) |
79 | 78 | 2ralbidv 2972 |
. . . . . . . 8
⊢ (𝑟 = (𝑧 / 2) → (∀𝑢 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧) ↔ ∀𝑢 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧))) |
80 | 79 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑧 / 2) ∈ ℝ+
∧ ∀𝑢 ∈
(Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < (𝑧 / 2) ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < (𝑧 / 2)) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) → ∃𝑟 ∈ ℝ+ ∀𝑢 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
81 | 12, 74, 80 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ ℝ+) →
∃𝑟 ∈
ℝ+ ∀𝑢 ∈ (Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
82 | 81 | ralrimiva 2949 |
. . . . 5
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑢 ∈
(Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
83 | 82 | ralrimivva 2954 |
. . . 4
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
∀𝑥 ∈
(Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑢 ∈
(Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)) |
84 | | msxms 22069 |
. . . . . 6
⊢ (𝐺 ∈ MetSp → 𝐺 ∈
∞MetSp) |
85 | | eqid 2610 |
. . . . . . 7
⊢
((dist‘𝐺)
↾ ((Base‘𝐺)
× (Base‘𝐺))) =
((dist‘𝐺) ↾
((Base‘𝐺) ×
(Base‘𝐺))) |
86 | 7, 85 | xmsxmet 22071 |
. . . . . 6
⊢ (𝐺 ∈ ∞MetSp →
((dist‘𝐺) ↾
((Base‘𝐺) ×
(Base‘𝐺))) ∈
(∞Met‘(Base‘𝐺))) |
87 | 4, 84, 86 | 3syl 18 |
. . . . 5
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
((dist‘𝐺) ↾
((Base‘𝐺) ×
(Base‘𝐺))) ∈
(∞Met‘(Base‘𝐺))) |
88 | | eqid 2610 |
. . . . . 6
⊢
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) = (MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) |
89 | 88, 88, 88 | txmetcn 22163 |
. . . . 5
⊢
((((dist‘𝐺)
↾ ((Base‘𝐺)
× (Base‘𝐺)))
∈ (∞Met‘(Base‘𝐺)) ∧ ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) ∈
(∞Met‘(Base‘𝐺)) ∧ ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) ∈
(∞Met‘(Base‘𝐺))) → ((-g‘𝐺) ∈
(((MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) ×t
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) Cn (MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) ↔
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑢 ∈
(Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)))) |
90 | 87, 87, 87, 89 | syl3anc 1318 |
. . . 4
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
((-g‘𝐺)
∈ (((MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) ×t
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) Cn (MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) ↔
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑢 ∈
(Base‘𝐺)∀𝑣 ∈ (Base‘𝐺)(((𝑥((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑢) < 𝑟 ∧ (𝑦((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))𝑣) < 𝑟) → ((𝑥(-g‘𝐺)𝑦)((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))(𝑢(-g‘𝐺)𝑣)) < 𝑧)))) |
91 | 10, 83, 90 | mpbir2and 959 |
. . 3
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
(-g‘𝐺)
∈ (((MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) ×t
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) Cn (MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))))) |
92 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
93 | 92, 7, 85 | mstopn 22067 |
. . . . . 6
⊢ (𝐺 ∈ MetSp →
(TopOpen‘𝐺) =
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) |
94 | 4, 93 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
(TopOpen‘𝐺) =
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) |
95 | 94, 94 | oveq12d 6567 |
. . . 4
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) = ((MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) ×t
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))))) |
96 | 95, 94 | oveq12d 6567 |
. . 3
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
(((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)) = (((MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))) ×t
(MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))))) Cn (MetOpen‘((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))))) |
97 | 91, 96 | eleqtrrd 2691 |
. 2
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) →
(-g‘𝐺)
∈ (((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
98 | 92, 8 | istgp2 21705 |
. 2
⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧
(-g‘𝐺)
∈ (((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))) |
99 | 2, 6, 97, 98 | syl3anbrc 1239 |
1
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel) → 𝐺 ∈ TopGrp) |