Step | Hyp | Ref
| Expression |
1 | | rrnequiv.d |
. . . . . 6
⊢ 𝐷 = (dist‘𝑌) |
2 | | ovex 6678 |
. . . . . . . 8
⊢
(ℂfld ↾s ℝ) ∈
V |
3 | | rrnequiv.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ Fin) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐼 ∈ Fin) |
5 | | rrnequiv.y |
. . . . . . . . 9
⊢ 𝑌 = ((ℂfld
↾s ℝ) ↑s 𝐼) |
6 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
7 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(ℂfld ↾s ℝ) =
(ℂfld ↾s ℝ) |
8 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Scalar‘ℂfld) =
(Scalar‘ℂfld) |
9 | 7, 8 | resssca 16031 |
. . . . . . . . . 10
⊢ (ℝ
∈ V → (Scalar‘ℂfld) =
(Scalar‘(ℂfld ↾s
ℝ))) |
10 | 6, 9 | ax-mp 5 |
. . . . . . . . 9
⊢
(Scalar‘ℂfld) =
(Scalar‘(ℂfld ↾s
ℝ)) |
11 | 5, 10 | pwsval 16146 |
. . . . . . . 8
⊢
(((ℂfld ↾s ℝ) ∈ V ∧
𝐼 ∈ Fin) → 𝑌 =
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
12 | 2, 4, 11 | sylancr 695 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝑌 =
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
13 | 12 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (dist‘𝑌) =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
14 | 1, 13 | syl5eq 2668 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐷 =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
15 | 14 | oveqd 6667 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) = (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld ↾s
ℝ)})))𝐺)) |
16 | | fconstmpt 5163 |
. . . . . 6
⊢ (𝐼 × {(ℂfld
↾s ℝ)}) = (𝑘 ∈ 𝐼 ↦ (ℂfld
↾s ℝ)) |
17 | 16 | oveq2i 6661 |
. . . . 5
⊢
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})) = ((Scalar‘ℂfld)Xs(𝑘 ∈ 𝐼 ↦ (ℂfld
↾s ℝ))) |
18 | | eqid 2622 |
. . . . 5
⊢
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) |
19 | | fvexd 6203 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(Scalar‘ℂfld) ∈ V) |
20 | 2 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (ℂfld
↾s ℝ) ∈ V) |
21 | 20 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (ℂfld ↾s
ℝ) ∈ V) |
22 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈ 𝑋) |
23 | | rrnequiv.1 |
. . . . . . 7
⊢ 𝑋 = (ℝ
↑𝑚 𝐼) |
24 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
25 | | cnfldbas 19750 |
. . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) |
26 | 7, 25 | ressbas2 15931 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ℝ = (Base‘(ℂfld
↾s ℝ))) |
27 | 24, 26 | ax-mp 5 |
. . . . . . . . . 10
⊢ ℝ =
(Base‘(ℂfld ↾s
ℝ)) |
28 | 5, 27 | pwsbas 16147 |
. . . . . . . . 9
⊢
(((ℂfld ↾s ℝ) ∈ V ∧
𝐼 ∈ Fin) →
(ℝ ↑𝑚 𝐼) = (Base‘𝑌)) |
29 | 2, 4, 28 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ℝ
↑𝑚 𝐼) = (Base‘𝑌)) |
30 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (Base‘𝑌) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
31 | 29, 30 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ℝ
↑𝑚 𝐼) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
32 | 23, 31 | syl5eq 2668 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝑋 =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
33 | 22, 32 | eleqtrd 2703 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
34 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈ 𝑋) |
35 | 34, 32 | eleqtrd 2703 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) |
36 | | cnfldds 19756 |
. . . . . . . 8
⊢ (abs
∘ − ) = (dist‘ℂfld) |
37 | 7, 36 | ressds 16073 |
. . . . . . 7
⊢ (ℝ
∈ V → (abs ∘ − ) = (dist‘(ℂfld
↾s ℝ))) |
38 | 6, 37 | ax-mp 5 |
. . . . . 6
⊢ (abs
∘ − ) = (dist‘(ℂfld ↾s
ℝ)) |
39 | 38 | reseq1i 5392 |
. . . . 5
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) =
((dist‘(ℂfld ↾s ℝ)) ↾
(ℝ × ℝ)) |
40 | | eqid 2622 |
. . . . 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 16145 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld ↾s
ℝ)})))𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ ×
ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
42 | 15, 41 | eqtrd 2656 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
43 | | eqid 2622 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
44 | 23, 43 | rrndstprj1 33629 |
. . . . . . . . 9
⊢ (((𝐼 ∈ Fin ∧ 𝑘 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
45 | 44 | an32s 846 |
. . . . . . . 8
⊢ (((𝐼 ∈ Fin ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
46 | 3, 45 | sylanl1 682 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
47 | 46 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
48 | | ovex 6678 |
. . . . . . . 8
⊢ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V |
49 | 48 | rgenw 2924 |
. . . . . . 7
⊢
∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V |
50 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) |
51 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑧 = ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) → (𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺))) |
52 | 50, 51 | ralrnmpt 6368 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V → (∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺))) |
53 | 49, 52 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑧 ∈
ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
54 | 47, 53 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
55 | 23 | rrnmet 33628 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
56 | 4, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
57 | | metge0 22150 |
. . . . . . . 8
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
58 | 56, 22, 34, 57 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
59 | | elsni 4194 |
. . . . . . . 8
⊢ (𝑧 ∈ {0} → 𝑧 = 0) |
60 | 59 | breq1d 4663 |
. . . . . . 7
⊢ (𝑧 ∈ {0} → (𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ 0 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
61 | 58, 60 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝑧 ∈ {0} → 𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
62 | 61 | ralrimiv 2965 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
63 | | ralunb 3794 |
. . . . 5
⊢
(∀𝑧 ∈
(ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ (∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
64 | 54, 62, 63 | sylanbrc 698 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) |
65 | 17, 18, 19, 4, 21, 27, 33 | prdsbascl 16143 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ ℝ) |
66 | 65 | r19.21bi 2932 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ) |
67 | 17, 18, 19, 4, 21, 27, 35 | prdsbascl 16143 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (𝐺‘𝑘) ∈ ℝ) |
68 | 67 | r19.21bi 2932 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ) |
69 | 43 | remet 22593 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(Met‘ℝ) |
70 | | metcl 22137 |
. . . . . . . . . . 11
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ)
∧ (𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
71 | 69, 70 | mp3an1 1411 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
72 | 66, 68, 71 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
73 | 72, 50 | fmptd 6385 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))):𝐼⟶ℝ) |
74 | | frn 6053 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))):𝐼⟶ℝ → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ ℝ) |
75 | 73, 74 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ ℝ) |
76 | | ressxr 10083 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
77 | 75, 76 | syl6ss 3615 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆
ℝ*) |
78 | | 0xr 10086 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
79 | 78 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ∈
ℝ*) |
80 | 79 | snssd 4340 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → {0} ⊆
ℝ*) |
81 | 77, 80 | unssd 3789 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆
ℝ*) |
82 | | metcl 22137 |
. . . . . . 7
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) |
83 | 56, 22, 34, 82 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) |
84 | 76, 83 | sseldi 3601 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ∈
ℝ*) |
85 | | supxrleub 12156 |
. . . . 5
⊢ (((ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆ ℝ*
∧ (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ*) →
(sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
86 | 81, 84, 85 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) |
87 | 64, 86 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺)) |
88 | 42, 87 | eqbrtrd 4675 |
. 2
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺)) |
89 | | rzal 4073 |
. . . . . . 7
⊢ (𝐼 = ∅ → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘)) |
90 | 22, 23 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈ (ℝ ↑𝑚
𝐼)) |
91 | | elmapi 7879 |
. . . . . . . . 9
⊢ (𝐹 ∈ (ℝ
↑𝑚 𝐼) → 𝐹:𝐼⟶ℝ) |
92 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:𝐼⟶ℝ → 𝐹 Fn 𝐼) |
93 | 90, 91, 92 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 Fn 𝐼) |
94 | 34, 23 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈ (ℝ ↑𝑚
𝐼)) |
95 | | elmapi 7879 |
. . . . . . . . 9
⊢ (𝐺 ∈ (ℝ
↑𝑚 𝐼) → 𝐺:𝐼⟶ℝ) |
96 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐺:𝐼⟶ℝ → 𝐺 Fn 𝐼) |
97 | 94, 95, 96 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 Fn 𝐼) |
98 | | eqfnfv 6311 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐼 ∧ 𝐺 Fn 𝐼) → (𝐹 = 𝐺 ↔ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘))) |
99 | 93, 97, 98 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹 = 𝐺 ↔ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘))) |
100 | 89, 99 | syl5ibr 236 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐼 = ∅ → 𝐹 = 𝐺)) |
101 | 100 | imp 445 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → 𝐹 = 𝐺) |
102 | 101 | oveq1d 6665 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn‘𝐼)𝐺) = (𝐺(ℝn‘𝐼)𝐺)) |
103 | | met0 22148 |
. . . . . . 7
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐺 ∈ 𝑋) → (𝐺(ℝn‘𝐼)𝐺) = 0) |
104 | 56, 34, 103 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐺(ℝn‘𝐼)𝐺) = 0) |
105 | | hashcl 13147 |
. . . . . . . . . 10
⊢ (𝐼 ∈ Fin →
(#‘𝐼) ∈
ℕ0) |
106 | 4, 105 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (#‘𝐼) ∈
ℕ0) |
107 | 106 | nn0red 11352 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (#‘𝐼) ∈ ℝ) |
108 | 106 | nn0ge0d 11354 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (#‘𝐼)) |
109 | 107, 108 | resqrtcld 14156 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (√‘(#‘𝐼)) ∈
ℝ) |
110 | 5, 1, 23 | repwsmet 33633 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋)) |
111 | 4, 110 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐷 ∈ (Met‘𝑋)) |
112 | | metcl 22137 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) ∈ ℝ) |
113 | 111, 22, 34, 112 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) ∈ ℝ) |
114 | 107, 108 | sqrtge0d 14159 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤
(√‘(#‘𝐼))) |
115 | | metge0 22150 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ≤ (𝐹𝐷𝐺)) |
116 | 111, 22, 34, 115 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (𝐹𝐷𝐺)) |
117 | 109, 113,
114, 116 | mulge0d 10604 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤
((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
118 | 104, 117 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐺(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
119 | 118 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐺(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
120 | 102, 119 | eqbrtrd 4675 |
. . 3
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
121 | 83 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) |
122 | 109, 113 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) |
123 | 122 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) |
124 | | rpre 11839 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
125 | 124 | ad2antll 765 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) |
126 | 123, 125 | readdcld 10069 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟) ∈ ℝ) |
127 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin) |
128 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ≠ ∅) |
129 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (Fin ∖ {∅})
↔ (𝐼 ∈ Fin ∧
𝐼 ≠
∅)) |
130 | 127, 128,
129 | sylanbrc 698 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ (Fin ∖
{∅})) |
131 | 22 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐹 ∈ 𝑋) |
132 | 34 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐺 ∈ 𝑋) |
133 | 113 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℝ) |
134 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ+) |
135 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
((#‘𝐼) ∈ ℕ
↔ 𝐼 ≠
∅)) |
136 | 127, 135 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
((#‘𝐼) ∈ ℕ
↔ 𝐼 ≠
∅)) |
137 | 128, 136 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(#‘𝐼) ∈
ℕ) |
138 | 137 | nnrpd 11870 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(#‘𝐼) ∈
ℝ+) |
139 | 138 | rpsqrtcld 14150 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(#‘𝐼))
∈ ℝ+) |
140 | 134, 139 | rpdivcld 11889 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(#‘𝐼))) ∈
ℝ+) |
141 | 140 | rpred 11872 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(#‘𝐼))) ∈
ℝ) |
142 | 133, 141 | readdcld 10069 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ) |
143 | | 0red 10041 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ∈
ℝ) |
144 | 116 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ≤
(𝐹𝐷𝐺)) |
145 | 133, 140 | ltaddrpd 11905 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼))))) |
146 | 143, 133,
142, 144, 145 | lelttrd 10195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 <
((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼))))) |
147 | 142, 146 | elrpd 11869 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈
ℝ+) |
148 | 72 | adantlr 751 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) |
149 | 133 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) ∈ ℝ) |
150 | 142 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ) |
151 | 81 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆
ℝ*) |
152 | | ssun1 3776 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) |
153 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
154 | 50 | elrnmpt1 5374 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝐼 ∧ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))) |
155 | 153, 48, 154 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))) |
156 | 152, 155 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})) |
157 | | supxrub 12154 |
. . . . . . . . . . . . 13
⊢ (((ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆ ℝ*
∧ ((𝐹‘𝑘)((abs ∘ − ) ↾
(ℝ × ℝ))(𝐺‘𝑘)) ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
158 | 151, 156,
157 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
159 | 42 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) |
160 | 158, 159 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹𝐷𝐺)) |
161 | 145 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼))))) |
162 | 148, 149,
150, 160, 161 | lelttrd 10195 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼))))) |
163 | 162 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼))))) |
164 | 23, 43 | rrndstprj2 33630 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ+ ∧
∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))) → (𝐹(ℝn‘𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼)))) |
165 | 130, 131,
132, 147, 163, 164 | syl32anc 1334 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼)))) |
166 | 133 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℂ) |
167 | 141 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(#‘𝐼))) ∈
ℂ) |
168 | 109 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(#‘𝐼))
∈ ℝ) |
169 | 168 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(#‘𝐼))
∈ ℂ) |
170 | 166, 167,
169 | adddird 10065 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼))) = (((𝐹𝐷𝐺) · (√‘(#‘𝐼))) + ((𝑟 / (√‘(#‘𝐼))) · (√‘(#‘𝐼))))) |
171 | 166, 169 | mulcomd 10061 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) · (√‘(#‘𝐼))) =
((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
172 | 125 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℂ) |
173 | 139 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(#‘𝐼))
≠ 0) |
174 | 172, 169,
173 | divcan1d 10802 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝑟 / (√‘(#‘𝐼))) ·
(√‘(#‘𝐼))) = 𝑟) |
175 | 171, 174 | oveq12d 6668 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) · (√‘(#‘𝐼))) + ((𝑟 / (√‘(#‘𝐼))) · (√‘(#‘𝐼)))) =
(((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
176 | 170, 175 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼))) =
(((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
177 | 165, 176 | breqtrd 4679 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) < (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
178 | 121, 126,
177 | ltled 10185 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
179 | 178 | anassrs 680 |
. . . . 5
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
180 | 179 | ralrimiva 2966 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → ∀𝑟 ∈ ℝ+
(𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) |
181 | | alrple 12037 |
. . . . . 6
⊢ (((𝐹(ℝn‘𝐼)𝐺) ∈ ℝ ∧
((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) |
182 | 83, 122, 181 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) |
183 | 182 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) |
184 | 180, 183 | mpbird 247 |
. . 3
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
185 | 120, 184 | pm2.61dane 2881 |
. 2
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))) |
186 | 88, 185 | jca 554 |
1
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))) |