Step | Hyp | Ref
| Expression |
1 | | nghmghm 23632 |
. . . 4
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
2 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑇) =
(Base‘𝑇) |
4 | 2, 3 | ghmf 18626 |
. . . 4
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
5 | 1, 4 | syl 17 |
. . 3
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
6 | | simprr 773 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ+) |
7 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑆 normOp 𝑇) = (𝑆 normOp 𝑇) |
8 | 7 | nghmcl 23625 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → ((𝑆 normOp 𝑇)‘𝐹) ∈ ℝ) |
9 | | nghmrcl1 23630 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp) |
10 | | nghmrcl2 23631 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp) |
11 | 7 | nmoge0 23619 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ ((𝑆 normOp 𝑇)‘𝐹)) |
12 | 9, 10, 1, 11 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 0 ≤ ((𝑆 normOp 𝑇)‘𝐹)) |
13 | 8, 12 | ge0p1rpd 12658 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (((𝑆 normOp 𝑇)‘𝐹) + 1) ∈
ℝ+) |
14 | 13 | adantr 484 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) → (((𝑆 normOp 𝑇)‘𝐹) + 1) ∈
ℝ+) |
15 | 6, 14 | rpdivcld 12645 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) ∈
ℝ+) |
16 | | ngpms 23498 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ NrmGrp → 𝑆 ∈ MetSp) |
17 | 9, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ MetSp) |
18 | 17 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ MetSp) |
19 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑆)) |
20 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑦 ∈ (Base‘𝑆)) |
21 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(dist‘𝑆) =
(dist‘𝑆) |
22 | 2, 21 | mscl 23359 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ MetSp ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(dist‘𝑆)𝑦) ∈ ℝ) |
23 | 18, 19, 20, 22 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(dist‘𝑆)𝑦) ∈ ℝ) |
24 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑟 ∈ ℝ+) |
25 | 24 | rpred 12628 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑟 ∈ ℝ) |
26 | 13 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝑆 normOp 𝑇)‘𝐹) + 1) ∈
ℝ+) |
27 | 23, 25, 26 | ltmuldiv2d 12676 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) < 𝑟 ↔ (𝑥(dist‘𝑆)𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)))) |
28 | | ngpms 23498 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp) |
29 | 10, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ MetSp) |
30 | 29 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑇 ∈ MetSp) |
31 | 5 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
32 | 31, 19 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘𝑥) ∈ (Base‘𝑇)) |
33 | 31, 20 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘𝑦) ∈ (Base‘𝑇)) |
34 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(dist‘𝑇) =
(dist‘𝑇) |
35 | 3, 34 | mscl 23359 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ MetSp ∧ (𝐹‘𝑥) ∈ (Base‘𝑇) ∧ (𝐹‘𝑦) ∈ (Base‘𝑇)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ∈ ℝ) |
36 | 30, 32, 33, 35 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ∈ ℝ) |
37 | 8 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑆 normOp 𝑇)‘𝐹) ∈ ℝ) |
38 | 37, 23 | remulcld 10863 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝑆 normOp 𝑇)‘𝐹) · (𝑥(dist‘𝑆)𝑦)) ∈ ℝ) |
39 | 26 | rpred 12628 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝑆 normOp 𝑇)‘𝐹) + 1) ∈ ℝ) |
40 | 39, 23 | remulcld 10863 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) ∈ ℝ) |
41 | 7, 2, 21, 34 | nmods 23642 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ≤ (((𝑆 normOp 𝑇)‘𝐹) · (𝑥(dist‘𝑆)𝑦))) |
42 | 41 | 3expa 1120 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ≤ (((𝑆 normOp 𝑇)‘𝐹) · (𝑥(dist‘𝑆)𝑦))) |
43 | 42 | adantlrr 721 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ≤ (((𝑆 normOp 𝑇)‘𝐹) · (𝑥(dist‘𝑆)𝑦))) |
44 | | msxms 23352 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ MetSp → 𝑆 ∈
∞MetSp) |
45 | 18, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 𝑆 ∈ ∞MetSp) |
46 | 2, 21 | xmsge0 23361 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ∞MetSp ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → 0 ≤ (𝑥(dist‘𝑆)𝑦)) |
47 | 45, 19, 20, 46 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → 0 ≤ (𝑥(dist‘𝑆)𝑦)) |
48 | 37 | lep1d 11763 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑆 normOp 𝑇)‘𝐹) ≤ (((𝑆 normOp 𝑇)‘𝐹) + 1)) |
49 | 37, 39, 23, 47, 48 | lemul1ad 11771 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝑆 normOp 𝑇)‘𝐹) · (𝑥(dist‘𝑆)𝑦)) ≤ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦))) |
50 | 36, 38, 40, 43, 49 | letrd 10989 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ≤ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦))) |
51 | | lelttr 10923 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ∈ ℝ ∧ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ≤ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) ∧ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) < 𝑟) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) < 𝑟)) |
52 | 36, 40, 25, 51 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) ≤ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) ∧ ((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) < 𝑟) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) < 𝑟)) |
53 | 50, 52 | mpand 695 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((((𝑆 normOp 𝑇)‘𝐹) + 1) · (𝑥(dist‘𝑆)𝑦)) < 𝑟 → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) < 𝑟)) |
54 | 27, 53 | sylbird 263 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑥(dist‘𝑆)𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) → ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) < 𝑟)) |
55 | 19, 20 | ovresd 7375 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) = (𝑥(dist‘𝑆)𝑦)) |
56 | 55 | breq1d 5063 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) ↔ (𝑥(dist‘𝑆)𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)))) |
57 | 32, 33 | ovresd 7375 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) = ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦))) |
58 | 57 | breq1d 5063 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → (((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟 ↔ ((𝐹‘𝑥)(dist‘𝑇)(𝐹‘𝑦)) < 𝑟)) |
59 | 54, 56, 58 | 3imtr4d 297 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)) |
60 | 59 | ralrimiva 3105 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) →
∀𝑦 ∈
(Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)) |
61 | | breq2 5057 |
. . . . . 6
⊢ (𝑠 = (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) → ((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑠 ↔ (𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)))) |
62 | 61 | rspceaimv 3542 |
. . . . 5
⊢ (((𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) ∈ ℝ+ ∧
∀𝑦 ∈
(Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < (𝑟 / (((𝑆 normOp 𝑇)‘𝐹) + 1)) → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)) → ∃𝑠 ∈ ℝ+ ∀𝑦 ∈ (Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑠 → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)) |
63 | 15, 60, 62 | syl2anc 587 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑟 ∈ ℝ+)) →
∃𝑠 ∈
ℝ+ ∀𝑦 ∈ (Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑠 → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)) |
64 | 63 | ralrimivva 3112 |
. . 3
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → ∀𝑥 ∈ (Base‘𝑆)∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑦 ∈
(Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑠 → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)) |
65 | | eqid 2737 |
. . . . . 6
⊢
((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆))) =
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) |
66 | 2, 65 | xmsxmet 23354 |
. . . . 5
⊢ (𝑆 ∈ ∞MetSp →
((dist‘𝑆) ↾
((Base‘𝑆) ×
(Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) |
67 | 17, 44, 66 | 3syl 18 |
. . . 4
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → ((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))) ∈
(∞Met‘(Base‘𝑆))) |
68 | | msxms 23352 |
. . . . 5
⊢ (𝑇 ∈ MetSp → 𝑇 ∈
∞MetSp) |
69 | | eqid 2737 |
. . . . . 6
⊢
((dist‘𝑇)
↾ ((Base‘𝑇)
× (Base‘𝑇))) =
((dist‘𝑇) ↾
((Base‘𝑇) ×
(Base‘𝑇))) |
70 | 3, 69 | xmsxmet 23354 |
. . . . 5
⊢ (𝑇 ∈ ∞MetSp →
((dist‘𝑇) ↾
((Base‘𝑇) ×
(Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) |
71 | 29, 68, 70 | 3syl 18 |
. . . 4
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) |
72 | | eqid 2737 |
. . . . 5
⊢
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) |
73 | | eqid 2737 |
. . . . 5
⊢
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))) |
74 | 72, 73 | metcn 23441 |
. . . 4
⊢
((((dist‘𝑆)
↾ ((Base‘𝑆)
× (Base‘𝑆)))
∈ (∞Met‘(Base‘𝑆)) ∧ ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(∞Met‘(Base‘𝑇))) → (𝐹 ∈ ((MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) Cn
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) ↔ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑦 ∈
(Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑠 → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)))) |
75 | 67, 71, 74 | syl2anc 587 |
. . 3
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝐹 ∈ ((MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) Cn
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) ↔ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑦 ∈
(Base‘𝑆)((𝑥((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))𝑦) < 𝑠 → ((𝐹‘𝑥)((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))(𝐹‘𝑦)) < 𝑟)))) |
76 | 5, 64, 75 | mpbir2and 713 |
. 2
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ ((MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) Cn
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))))) |
77 | | nghmcn.j |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝑆) |
78 | 77, 2, 65 | mstopn 23350 |
. . . 4
⊢ (𝑆 ∈ MetSp → 𝐽 =
(MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) |
79 | 17, 78 | syl 17 |
. . 3
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐽 = (MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆))))) |
80 | | nghmcn.k |
. . . . 5
⊢ 𝐾 = (TopOpen‘𝑇) |
81 | 80, 3, 69 | mstopn 23350 |
. . . 4
⊢ (𝑇 ∈ MetSp → 𝐾 =
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
82 | 29, 81 | syl 17 |
. . 3
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐾 = (MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
83 | 79, 82 | oveq12d 7231 |
. 2
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝐽 Cn 𝐾) = ((MetOpen‘((dist‘𝑆) ↾ ((Base‘𝑆) × (Base‘𝑆)))) Cn
(MetOpen‘((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇)))))) |
84 | 76, 83 | eleqtrrd 2841 |
1
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) |