Step | Hyp | Ref
| Expression |
1 | | rrnequiv.d |
. . . . . 6
⊢ 𝐷 = (dist‘𝑌) |
2 | | ovex 7246 |
. . . . . . . 8
⊢
(ℂfld ↾s ℝ) ∈
V |
3 | | rrnequiv.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ Fin) |
4 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐼 ∈ Fin) |
5 | | rrnequiv.y |
. . . . . . . . 9
⊢ 𝑌 = ((ℂfld
↾s ℝ) ↑s 𝐼) |
6 | | reex 10820 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
7 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(ℂfld ↾s ℝ) =
(ℂfld ↾s ℝ) |
8 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Scalar‘ℂfld) =
(Scalar‘ℂfld) |
9 | 7, 8 | resssca 16876 |
. . . . . . . . . 10
⊢ (ℝ
∈ V → (Scalar‘ℂfld) =
(Scalar‘(ℂfld ↾s
ℝ))) |
10 | 6, 9 | ax-mp 5 |
. . . . . . . . 9
⊢
(Scalar‘ℂfld) =
(Scalar‘(ℂfld ↾s
ℝ)) |
11 | 5, 10 | pwsval 16991 |
. . . . . . . 8
⊢
(((ℂfld ↾s ℝ) ∈ V ∧
𝐼 ∈ Fin) → 𝑌 =
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
12 | 2, 4, 11 | sylancr 590 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝑌 =
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
13 | 12 | fveq2d 6721 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (dist‘𝑌) =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
14 | 1, 13 | syl5eq 2790 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐷 =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
15 | 14 | oveqd 7230 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) = (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld ↾s
ℝ)})))𝐺)) |
16 | | fconstmpt 5611 |
. . . . . 6
⊢ (𝐼 × {(ℂfld
↾s ℝ)}) = (𝑘 ∈ 𝐼 ↦ (ℂfld
↾s ℝ)) |
17 | 16 | oveq2i 7224 |
. . . . 5
⊢
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})) = ((Scalar‘ℂfld)Xs(𝑘 ∈ 𝐼 ↦ (ℂfld
↾s ℝ))) |
18 | | eqid 2737 |
. . . . 5
⊢
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
19 | | fvexd 6732 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(Scalar‘ℂfld) ∈ V) |
20 | 2 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (ℂfld
↾s ℝ) ∈ V) |
21 | 20 | ralrimiva 3105 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (ℂfld ↾s
ℝ) ∈ V) |
22 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈ 𝑋) |
23 | | rrnequiv.1 |
. . . . . . 7
⊢ 𝑋 = (ℝ ↑m
𝐼) |
24 | | ax-resscn 10786 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
25 | | cnfldbas 20367 |
. . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) |
26 | 7, 25 | ressbas2 16791 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ℝ = (Base‘(ℂfld
↾s ℝ))) |
27 | 24, 26 | ax-mp 5 |
. . . . . . . . . 10
⊢ ℝ =
(Base‘(ℂfld ↾s
ℝ)) |
28 | 5, 27 | pwsbas 16992 |
. . . . . . . . 9
⊢
(((ℂfld ↾s ℝ) ∈ V ∧
𝐼 ∈ Fin) →
(ℝ ↑m 𝐼) = (Base‘𝑌)) |
29 | 2, 4, 28 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ℝ ↑m 𝐼) = (Base‘𝑌)) |
30 | 12 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (Base‘𝑌) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
31 | 29, 30 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ℝ ↑m 𝐼) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
32 | 23, 31 | syl5eq 2790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝑋 =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
33 | 22, 32 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
34 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈ 𝑋) |
35 | 34, 32 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
36 | | cnfldds 20373 |
. . . . . . . 8
⊢ (abs
∘ − ) = (dist‘ℂfld) |
37 | 7, 36 | ressds 16917 |
. . . . . . 7
⊢ (ℝ
∈ V → (abs ∘ − ) = (dist‘(ℂfld
↾s ℝ))) |
38 | 6, 37 | ax-mp 5 |
. . . . . 6
⊢ (abs
∘ − ) = (dist‘(ℂfld ↾s
ℝ)) |
39 | 38 | reseq1i 5847 |
. . . . 5
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) =
((dist‘(ℂfld ↾s ℝ)) ↾
(ℝ × ℝ)) |
40 | | eqid 2737 |
. . . . 5
⊢
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
41 | 17, 18, 19, 4, 21, 33, 35, 27, 39, 40 | prdsdsval3 16990 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld ↾s
ℝ)})))𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ ×
ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
42 | 15, 41 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
43 | | eqid 2737 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
44 | 23, 43 | rrndstprj1 35725 |
. . . . . . . . 9
⊢ (((𝐼 ∈ Fin ∧ 𝑘 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
45 | 44 | an32s 652 |
. . . . . . . 8
⊢ (((𝐼 ∈ Fin ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
46 | 3, 45 | sylanl1 680 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
47 | 46 | ralrimiva 3105 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
48 | | ovex 7246 |
. . . . . . . 8
⊢ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V |
49 | 48 | rgenw 3073 |
. . . . . . 7
⊢
∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V |
50 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) |
51 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑧 = ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) → (𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺))) |
52 | 50, 51 | ralrnmptw 6913 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V → (∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺))) |
53 | 49, 52 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑧 ∈
ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
54 | 47, 53 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
55 | 23 | rrnmet 35724 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
56 | 4, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
57 | | metge0 23243 |
. . . . . . . 8
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
58 | 56, 22, 34, 57 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
59 | | elsni 4558 |
. . . . . . . 8
⊢ (𝑧 ∈ {0} → 𝑧 = 0) |
60 | 59 | breq1d 5063 |
. . . . . . 7
⊢ (𝑧 ∈ {0} → (𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ 0 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
61 | 58, 60 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝑧 ∈ {0} → 𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
62 | 61 | ralrimiv 3104 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
63 | | ralunb 4105 |
. . . . 5
⊢
(∀𝑧 ∈
(ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ (∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
64 | 54, 62, 63 | sylanbrc 586 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
65 | 17, 18, 19, 4, 21, 27, 33 | prdsbascl 16988 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ ℝ) |
66 | 65 | r19.21bi 3130 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ) |
67 | 17, 18, 19, 4, 21, 27, 35 | prdsbascl 16988 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (𝐺‘𝑘) ∈ ℝ) |
68 | 67 | r19.21bi 3130 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ) |
69 | 43 | remet 23687 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(Met‘ℝ) |
70 | | metcl 23230 |
. . . . . . . . . . 11
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ)
∧ (𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
71 | 69, 70 | mp3an1 1450 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
72 | 66, 68, 71 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
73 | 72 | fmpttd 6932 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))):𝐼⟶ℝ) |
74 | 73 | frnd 6553 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ ℝ) |
75 | | ressxr 10877 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
76 | 74, 75 | sstrdi 3913 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆
ℝ*) |
77 | | 0xr 10880 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
78 | 77 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ∈
ℝ*) |
79 | 78 | snssd 4722 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → {0} ⊆
ℝ*) |
80 | 76, 79 | unssd 4100 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆
ℝ*) |
81 | | metcl 23230 |
. . . . . . 7
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) |
82 | 56, 22, 34, 81 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) |
83 | 75, 82 | sseldi 3899 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ∈
ℝ*) |
84 | | supxrleub 12916 |
. . . . 5
⊢ (((ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆ ℝ*
∧ (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ*) →
(sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
85 | 80, 83, 84 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
86 | 64, 85 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺)) |
87 | 42, 86 | eqbrtrd 5075 |
. 2
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
88 | | rzal 4420 |
. . . . . . 7
⊢ (𝐼 = ∅ → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘)) |
89 | 22, 23 | eleqtrdi 2848 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈ (ℝ ↑m 𝐼)) |
90 | | elmapi 8530 |
. . . . . . . . 9
⊢ (𝐹 ∈ (ℝ
↑m 𝐼)
→ 𝐹:𝐼⟶ℝ) |
91 | | ffn 6545 |
. . . . . . . . 9
⊢ (𝐹:𝐼⟶ℝ → 𝐹 Fn 𝐼) |
92 | 89, 90, 91 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 Fn 𝐼) |
93 | 34, 23 | eleqtrdi 2848 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈ (ℝ ↑m 𝐼)) |
94 | | elmapi 8530 |
. . . . . . . . 9
⊢ (𝐺 ∈ (ℝ
↑m 𝐼)
→ 𝐺:𝐼⟶ℝ) |
95 | | ffn 6545 |
. . . . . . . . 9
⊢ (𝐺:𝐼⟶ℝ → 𝐺 Fn 𝐼) |
96 | 93, 94, 95 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 Fn 𝐼) |
97 | | eqfnfv 6852 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐼 ∧ 𝐺 Fn 𝐼) → (𝐹 = 𝐺 ↔ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘))) |
98 | 92, 96, 97 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹 = 𝐺 ↔ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘))) |
99 | 88, 98 | syl5ibr 249 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐼 = ∅ → 𝐹 = 𝐺)) |
100 | 99 | imp 410 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → 𝐹 = 𝐺) |
101 | 100 | oveq1d 7228 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn‘𝐼)𝐺) = (𝐺(ℝn‘𝐼)𝐺)) |
102 | | met0 23241 |
. . . . . . 7
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐺 ∈ 𝑋) → (𝐺(ℝn‘𝐼)𝐺) = 0) |
103 | 56, 34, 102 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐺(ℝn‘𝐼)𝐺) = 0) |
104 | | hashcl 13923 |
. . . . . . . . . 10
⊢ (𝐼 ∈ Fin →
(♯‘𝐼) ∈
ℕ0) |
105 | 4, 104 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (♯‘𝐼) ∈
ℕ0) |
106 | 105 | nn0red 12151 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (♯‘𝐼) ∈ ℝ) |
107 | 105 | nn0ge0d 12153 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (♯‘𝐼)) |
108 | 106, 107 | resqrtcld 14981 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(√‘(♯‘𝐼)) ∈ ℝ) |
109 | 5, 1, 23 | repwsmet 35729 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋)) |
110 | 4, 109 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐷 ∈ (Met‘𝑋)) |
111 | | metcl 23230 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) ∈ ℝ) |
112 | 110, 22, 34, 111 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) ∈ ℝ) |
113 | 106, 107 | sqrtge0d 14984 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤
(√‘(♯‘𝐼))) |
114 | | metge0 23243 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ≤ (𝐹𝐷𝐺)) |
115 | 110, 22, 34, 114 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (𝐹𝐷𝐺)) |
116 | 108, 112,
113, 115 | mulge0d 11409 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
117 | 103, 116 | eqbrtrd 5075 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐺(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
118 | 117 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐺(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
119 | 101, 118 | eqbrtrd 5075 |
. . 3
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
120 | 82 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) |
121 | 108, 112 | remulcld 10863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) |
122 | 121 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) |
123 | | rpre 12594 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
124 | 123 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) |
125 | 122, 124 | readdcld 10862 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟) ∈ ℝ) |
126 | 4 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin) |
127 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ≠ ∅) |
128 | | eldifsn 4700 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (Fin ∖ {∅})
↔ (𝐼 ∈ Fin ∧
𝐼 ≠
∅)) |
129 | 126, 127,
128 | sylanbrc 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ (Fin ∖
{∅})) |
130 | 22 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐹 ∈ 𝑋) |
131 | 34 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐺 ∈ 𝑋) |
132 | 112 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℝ) |
133 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ+) |
134 | | hashnncl 13933 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) |
135 | 126, 134 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) |
136 | 127, 135 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(♯‘𝐼) ∈
ℕ) |
137 | 136 | nnrpd 12626 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(♯‘𝐼) ∈
ℝ+) |
138 | 137 | rpsqrtcld 14975 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ∈
ℝ+) |
139 | 133, 138 | rpdivcld 12645 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 /
(√‘(♯‘𝐼))) ∈
ℝ+) |
140 | 139 | rpred 12628 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 /
(√‘(♯‘𝐼))) ∈ ℝ) |
141 | 132, 140 | readdcld 10862 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈
ℝ) |
142 | | 0red 10836 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ∈
ℝ) |
143 | 115 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ≤
(𝐹𝐷𝐺)) |
144 | 132, 139 | ltaddrpd 12661 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) |
145 | 142, 132,
141, 143, 144 | lelttrd 10990 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 <
((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) |
146 | 141, 145 | elrpd 12625 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈
ℝ+) |
147 | 72 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
148 | 132 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) ∈ ℝ) |
149 | 141 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈
ℝ) |
150 | 80 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆
ℝ*) |
151 | | ssun1 4086 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) |
152 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
153 | 50 | elrnmpt1 5827 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝐼 ∧ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))) |
154 | 152, 48, 153 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))) |
155 | 151, 154 | sseldi 3899 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})) |
156 | | supxrub 12914 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆ ℝ*
∧ ((𝐹‘𝑘)((abs ∘ − ) ↾
(ℝ × ℝ))(𝐺‘𝑘)) ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
157 | 150, 155,
156 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
158 | 42 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
159 | 157, 158 | breqtrrd 5081 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹𝐷𝐺)) |
160 | 144 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) |
161 | 147, 148,
149, 159, 160 | lelttrd 10990 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) |
162 | 161 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) |
163 | 23, 43 | rrndstprj2 35726 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈ ℝ+
∧ ∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))) → (𝐹(ℝn‘𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼)))) |
164 | 129, 130,
131, 146, 162, 163 | syl32anc 1380 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼)))) |
165 | 132 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℂ) |
166 | 140 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 /
(√‘(♯‘𝐼))) ∈ ℂ) |
167 | 108 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ∈ ℝ) |
168 | 167 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ∈ ℂ) |
169 | 165, 166,
168 | adddird 10858 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼))) = (((𝐹𝐷𝐺) ·
(√‘(♯‘𝐼))) + ((𝑟 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))))) |
170 | 165, 168 | mulcomd 10854 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) ·
(√‘(♯‘𝐼))) = ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
171 | 124 | recnd 10861 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℂ) |
172 | 138 | rpne0d 12633 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ≠ 0) |
173 | 171, 168,
172 | divcan1d 11609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝑟 /
(√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))) = 𝑟) |
174 | 170, 173 | oveq12d 7231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) ·
(√‘(♯‘𝐼))) + ((𝑟 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼)))) = (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
175 | 169, 174 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼))) = (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
176 | 164, 175 | breqtrd 5079 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) < (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
177 | 120, 125,
176 | ltled 10980 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
178 | 177 | anassrs 471 |
. . . . 5
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
179 | 178 | ralrimiva 3105 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → ∀𝑟 ∈ ℝ+
(𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
180 | | alrple 12796 |
. . . . . 6
⊢ (((𝐹(ℝn‘𝐼)𝐺) ∈ ℝ ∧
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) |
181 | 82, 121, 180 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) |
182 | 181 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) |
183 | 179, 182 | mpbird 260 |
. . 3
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
184 | 119, 183 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) |
185 | 87, 184 | jca 515 |
1
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))) |