| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rrnequiv.d | . . . . . 6
⊢ 𝐷 = (dist‘𝑌) | 
| 2 |  | ovex 7464 | . . . . . . . 8
⊢
(ℂfld ↾s ℝ) ∈
V | 
| 3 |  | rrnequiv.i | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ Fin) | 
| 4 | 3 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐼 ∈ Fin) | 
| 5 |  | rrnequiv.y | . . . . . . . . 9
⊢ 𝑌 = ((ℂfld
↾s ℝ) ↑s 𝐼) | 
| 6 |  | reex 11246 | . . . . . . . . . 10
⊢ ℝ
∈ V | 
| 7 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(ℂfld ↾s ℝ) =
(ℂfld ↾s ℝ) | 
| 8 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Scalar‘ℂfld) =
(Scalar‘ℂfld) | 
| 9 | 7, 8 | resssca 17387 | . . . . . . . . . 10
⊢ (ℝ
∈ V → (Scalar‘ℂfld) =
(Scalar‘(ℂfld ↾s
ℝ))) | 
| 10 | 6, 9 | ax-mp 5 | . . . . . . . . 9
⊢
(Scalar‘ℂfld) =
(Scalar‘(ℂfld ↾s
ℝ)) | 
| 11 | 5, 10 | pwsval 17531 | . . . . . . . 8
⊢
(((ℂfld ↾s ℝ) ∈ V ∧
𝐼 ∈ Fin) → 𝑌 =
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) | 
| 12 | 2, 4, 11 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝑌 =
((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)}))) | 
| 13 | 12 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (dist‘𝑌) =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 14 | 1, 13 | eqtrid 2789 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐷 =
(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 15 | 14 | oveqd 7448 | . . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) = (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld ↾s
ℝ)})))𝐺)) | 
| 16 |  | fconstmpt 5747 | . . . . . 6
⊢ (𝐼 × {(ℂfld
↾s ℝ)}) = (𝑘 ∈ 𝐼 ↦ (ℂfld
↾s ℝ)) | 
| 17 | 16 | oveq2i 7442 | . . . . 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 6921 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(Scalar‘ℂfld) ∈ V) | 
| 20 | 2 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (ℂfld
↾s ℝ) ∈ V) | 
| 21 | 20 | ralrimiva 3146 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (ℂfld ↾s
ℝ) ∈ V) | 
| 22 |  | simprl 771 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈ 𝑋) | 
| 23 |  | rrnequiv.1 | . . . . . . 7
⊢ 𝑋 = (ℝ ↑m
𝐼) | 
| 24 |  | ax-resscn 11212 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℂ | 
| 25 |  | cnfldbas 21368 | . . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) | 
| 26 | 7, 25 | ressbas2 17283 | . . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ℝ = (Base‘(ℂfld
↾s ℝ))) | 
| 27 | 24, 26 | ax-mp 5 | . . . . . . . . . 10
⊢ ℝ =
(Base‘(ℂfld ↾s
ℝ)) | 
| 28 | 5, 27 | pwsbas 17532 | . . . . . . . . 9
⊢
(((ℂfld ↾s ℝ) ∈ V ∧
𝐼 ∈ Fin) →
(ℝ ↑m 𝐼) = (Base‘𝑌)) | 
| 29 | 2, 4, 28 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ℝ ↑m 𝐼) = (Base‘𝑌)) | 
| 30 | 12 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (Base‘𝑌) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 31 | 29, 30 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ℝ ↑m 𝐼) =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 32 | 23, 31 | eqtrid 2789 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝑋 =
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 33 | 22, 32 | eleqtrd 2843 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 34 |  | simprr 773 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈ 𝑋) | 
| 35 | 34, 32 | eleqtrd 2843 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈
(Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂfld
↾s ℝ)})))) | 
| 36 |  | cnfldds 21376 | . . . . . . . 8
⊢ (abs
∘ − ) = (dist‘ℂfld) | 
| 37 | 7, 36 | ressds 17454 | . . . . . . 7
⊢ (ℝ
∈ V → (abs ∘ − ) = (dist‘(ℂfld
↾s ℝ))) | 
| 38 | 6, 37 | ax-mp 5 | . . . . . 6
⊢ (abs
∘ − ) = (dist‘(ℂfld ↾s
ℝ)) | 
| 39 | 38 | reseq1i 5993 | . . . . 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 17530 | . . . 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 37837 | . . . . . . . . 9
⊢ (((𝐼 ∈ Fin ∧ 𝑘 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 45 | 44 | an32s 652 | . . . . . . . 8
⊢ (((𝐼 ∈ Fin ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 46 | 3, 45 | sylanl1 680 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 47 | 46 | ralrimiva 3146 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 48 |  | ovex 7464 | . . . . . . . 8
⊢ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V | 
| 49 | 48 | rgenw 3065 | . . . . . . 7
⊢
∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V | 
| 50 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) | 
| 51 |  | breq1 5146 | . . . . . . . 8
⊢ (𝑧 = ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) → (𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 52 | 50, 51 | ralrnmptw 7114 | . . . . . . 7
⊢
(∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V → (∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 53 | 49, 52 | ax-mp 5 | . . . . . 6
⊢
(∀𝑧 ∈
ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 54 | 47, 53 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 55 | 23 | rrnmet 37836 | . . . . . . . . 9
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) | 
| 56 | 4, 55 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(ℝn‘𝐼) ∈ (Met‘𝑋)) | 
| 57 |  | metge0 24355 | . . . . . . . 8
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 58 | 56, 22, 34, 57 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 59 |  | elsni 4643 | . . . . . . . 8
⊢ (𝑧 ∈ {0} → 𝑧 = 0) | 
| 60 | 59 | breq1d 5153 | . . . . . . 7
⊢ (𝑧 ∈ {0} → (𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ 0 ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 61 | 58, 60 | syl5ibrcom 247 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝑧 ∈ {0} → 𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 62 | 61 | ralrimiv 3145 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 63 |  | ralunb 4197 | . . . . 5
⊢
(∀𝑧 ∈
(ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ↔ (∀𝑧 ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 64 | 54, 62, 63 | sylanbrc 583 | . . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 65 | 17, 18, 19, 4, 21, 27, 33 | prdsbascl 17528 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) ∈ ℝ) | 
| 66 | 65 | r19.21bi 3251 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ) | 
| 67 | 17, 18, 19, 4, 21, 27, 35 | prdsbascl 17528 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ∀𝑘 ∈ 𝐼 (𝐺‘𝑘) ∈ ℝ) | 
| 68 | 67 | r19.21bi 3251 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ) | 
| 69 | 43 | remet 24811 | . . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(Met‘ℝ) | 
| 70 |  | metcl 24342 | . . . . . . . . . . 11
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ)
∧ (𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) | 
| 71 | 69, 70 | mp3an1 1450 | . . . . . . . . . 10
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) | 
| 72 | 66, 68, 71 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) | 
| 73 | 72 | fmpttd 7135 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))):𝐼⟶ℝ) | 
| 74 | 73 | frnd 6744 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ ℝ) | 
| 75 |  | ressxr 11305 | . . . . . . 7
⊢ ℝ
⊆ ℝ* | 
| 76 | 74, 75 | sstrdi 3996 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆
ℝ*) | 
| 77 |  | 0xr 11308 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 78 | 77 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ∈
ℝ*) | 
| 79 | 78 | snssd 4809 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → {0} ⊆
ℝ*) | 
| 80 | 76, 79 | unssd 4192 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆
ℝ*) | 
| 81 |  | metcl 24342 | . . . . . . 7
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) | 
| 82 | 56, 22, 34, 81 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) | 
| 83 | 75, 82 | sselid 3981 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ∈
ℝ*) | 
| 84 |  | supxrleub 13368 | . . . . 5
⊢ (((ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆ ℝ*
∧ (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ*) →
(sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 85 | 80, 83, 84 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn‘𝐼)𝐺))) | 
| 86 | 64, 85 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, < )
≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 87 | 42, 86 | eqbrtrd 5165 | . 2
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺)) | 
| 88 |  | rzal 4509 | . . . . . . 7
⊢ (𝐼 = ∅ → ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘)) | 
| 89 | 22, 23 | eleqtrdi 2851 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 ∈ (ℝ ↑m 𝐼)) | 
| 90 |  | elmapi 8889 | . . . . . . . . 9
⊢ (𝐹 ∈ (ℝ
↑m 𝐼)
→ 𝐹:𝐼⟶ℝ) | 
| 91 |  | ffn 6736 | . . . . . . . . 9
⊢ (𝐹:𝐼⟶ℝ → 𝐹 Fn 𝐼) | 
| 92 | 89, 90, 91 | 3syl 18 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐹 Fn 𝐼) | 
| 93 | 34, 23 | eleqtrdi 2851 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 ∈ (ℝ ↑m 𝐼)) | 
| 94 |  | elmapi 8889 | . . . . . . . . 9
⊢ (𝐺 ∈ (ℝ
↑m 𝐼)
→ 𝐺:𝐼⟶ℝ) | 
| 95 |  | ffn 6736 | . . . . . . . . 9
⊢ (𝐺:𝐼⟶ℝ → 𝐺 Fn 𝐼) | 
| 96 | 93, 94, 95 | 3syl 18 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐺 Fn 𝐼) | 
| 97 |  | eqfnfv 7051 | . . . . . . . 8
⊢ ((𝐹 Fn 𝐼 ∧ 𝐺 Fn 𝐼) → (𝐹 = 𝐺 ↔ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘))) | 
| 98 | 92, 96, 97 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹 = 𝐺 ↔ ∀𝑘 ∈ 𝐼 (𝐹‘𝑘) = (𝐺‘𝑘))) | 
| 99 | 88, 98 | imbitrrid 246 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐼 = ∅ → 𝐹 = 𝐺)) | 
| 100 | 99 | imp 406 | . . . . 5
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → 𝐹 = 𝐺) | 
| 101 | 100 | oveq1d 7446 | . . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn‘𝐼)𝐺) = (𝐺(ℝn‘𝐼)𝐺)) | 
| 102 |  | met0 24353 | . . . . . . 7
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ 𝐺 ∈ 𝑋) → (𝐺(ℝn‘𝐼)𝐺) = 0) | 
| 103 | 56, 34, 102 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐺(ℝn‘𝐼)𝐺) = 0) | 
| 104 |  | hashcl 14395 | . . . . . . . . . 10
⊢ (𝐼 ∈ Fin →
(♯‘𝐼) ∈
ℕ0) | 
| 105 | 4, 104 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (♯‘𝐼) ∈
ℕ0) | 
| 106 | 105 | nn0red 12588 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (♯‘𝐼) ∈ ℝ) | 
| 107 | 105 | nn0ge0d 12590 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (♯‘𝐼)) | 
| 108 | 106, 107 | resqrtcld 15456 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
(√‘(♯‘𝐼)) ∈ ℝ) | 
| 109 | 5, 1, 23 | repwsmet 37841 | . . . . . . . . 9
⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋)) | 
| 110 | 4, 109 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 𝐷 ∈ (Met‘𝑋)) | 
| 111 |  | metcl 24342 | . . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) ∈ ℝ) | 
| 112 | 110, 22, 34, 111 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹𝐷𝐺) ∈ ℝ) | 
| 113 | 106, 107 | sqrtge0d 15459 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤
(√‘(♯‘𝐼))) | 
| 114 |  | metge0 24355 | . . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → 0 ≤ (𝐹𝐷𝐺)) | 
| 115 | 110, 22, 34, 114 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤ (𝐹𝐷𝐺)) | 
| 116 | 108, 112,
113, 115 | mulge0d 11840 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → 0 ≤
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 117 | 103, 116 | eqbrtrd 5165 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐺(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 118 | 117 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐺(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 119 | 101, 118 | eqbrtrd 5165 | . . 3
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 120 | 82 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) ∈ ℝ) | 
| 121 | 108, 112 | remulcld 11291 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) →
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) | 
| 122 | 121 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) | 
| 123 |  | rpre 13043 | . . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) | 
| 124 | 123 | ad2antll 729 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ) | 
| 125 | 122, 124 | readdcld 11290 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟) ∈ ℝ) | 
| 126 | 4 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin) | 
| 127 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ≠ ∅) | 
| 128 |  | eldifsn 4786 | . . . . . . . . . 10
⊢ (𝐼 ∈ (Fin ∖ {∅})
↔ (𝐼 ∈ Fin ∧
𝐼 ≠
∅)) | 
| 129 | 126, 127,
128 | sylanbrc 583 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ (Fin ∖
{∅})) | 
| 130 | 22 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐹 ∈ 𝑋) | 
| 131 | 34 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐺 ∈ 𝑋) | 
| 132 | 112 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℝ) | 
| 133 |  | simprr 773 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ+) | 
| 134 |  | hashnncl 14405 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) | 
| 135 | 126, 134 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) | 
| 136 | 127, 135 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(♯‘𝐼) ∈
ℕ) | 
| 137 | 136 | nnrpd 13075 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(♯‘𝐼) ∈
ℝ+) | 
| 138 | 137 | rpsqrtcld 15450 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ∈
ℝ+) | 
| 139 | 133, 138 | rpdivcld 13094 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 /
(√‘(♯‘𝐼))) ∈
ℝ+) | 
| 140 | 139 | rpred 13077 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 /
(√‘(♯‘𝐼))) ∈ ℝ) | 
| 141 | 132, 140 | readdcld 11290 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈
ℝ) | 
| 142 |  | 0red 11264 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ∈
ℝ) | 
| 143 | 115 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ≤
(𝐹𝐷𝐺)) | 
| 144 | 132, 139 | ltaddrpd 13110 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) | 
| 145 | 142, 132,
141, 143, 144 | lelttrd 11419 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 <
((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) | 
| 146 | 141, 145 | elrpd 13074 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈
ℝ+) | 
| 147 | 72 | adantlr 715 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ℝ) | 
| 148 | 132 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) ∈ ℝ) | 
| 149 | 141 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈
ℝ) | 
| 150 | 80 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆
ℝ*) | 
| 151 |  | ssun1 4178 | . . . . . . . . . . . . . 14
⊢ ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ⊆ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) | 
| 152 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) | 
| 153 | 50 | elrnmpt1 5971 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝐼 ∧ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ V) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))) | 
| 154 | 152, 48, 153 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)))) | 
| 155 | 151, 154 | sselid 3981 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})) | 
| 156 |  | supxrub 13366 | . . . . . . . . . . . . 13
⊢ (((ran
(𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}) ⊆ ℝ*
∧ ((𝐹‘𝑘)((abs ∘ − ) ↾
(ℝ × ℝ))(𝐺‘𝑘)) ∈ (ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0})) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) | 
| 157 | 150, 155,
156 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) | 
| 158 | 42 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) = sup((ran (𝑘 ∈ 𝐼 ↦ ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘))) ∪ {0}), ℝ*, <
)) | 
| 159 | 157, 158 | breqtrrd 5171 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) ≤ (𝐹𝐷𝐺)) | 
| 160 | 144 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) | 
| 161 | 147, 148,
149, 159, 160 | lelttrd 11419 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) | 
| 162 | 161 | ralrimiva 3146 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
∀𝑘 ∈ 𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼))))) | 
| 163 | 23, 43 | rrndstprj2 37838 | . . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈ ℝ+
∧ ∀𝑘 ∈
𝐼 ((𝐹‘𝑘)((abs ∘ − ) ↾ (ℝ
× ℝ))(𝐺‘𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))) → (𝐹(ℝn‘𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼)))) | 
| 164 | 129, 130,
131, 146, 162, 163 | syl32anc 1380 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼)))) | 
| 165 | 132 | recnd 11289 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℂ) | 
| 166 | 140 | recnd 11289 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 /
(√‘(♯‘𝐼))) ∈ ℂ) | 
| 167 | 108 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ∈ ℝ) | 
| 168 | 167 | recnd 11289 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ∈ ℂ) | 
| 169 | 165, 166,
168 | adddird 11286 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼))) = (((𝐹𝐷𝐺) ·
(√‘(♯‘𝐼))) + ((𝑟 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))))) | 
| 170 | 165, 168 | mulcomd 11282 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) ·
(√‘(♯‘𝐼))) = ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 171 | 124 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℂ) | 
| 172 | 138 | rpne0d 13082 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) →
(√‘(♯‘𝐼)) ≠ 0) | 
| 173 | 171, 168,
172 | divcan1d 12044 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝑟 /
(√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))) = 𝑟) | 
| 174 | 170, 173 | oveq12d 7449 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) ·
(√‘(♯‘𝐼))) + ((𝑟 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼)))) = (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) | 
| 175 | 169, 174 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ·
(√‘(♯‘𝐼))) = (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) | 
| 176 | 164, 175 | breqtrd 5169 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) < (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) | 
| 177 | 120, 125,
176 | ltled 11409 | . . . . . 6
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) | 
| 178 | 177 | anassrs 467 | . . . . 5
⊢ ((((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) | 
| 179 | 178 | ralrimiva 3146 | . . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → ∀𝑟 ∈ ℝ+
(𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)) | 
| 180 |  | alrple 13248 | . . . . . 6
⊢ (((𝐹(ℝn‘𝐼)𝐺) ∈ ℝ ∧
((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) | 
| 181 | 82, 121, 180 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) | 
| 182 | 181 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → ((𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn‘𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))) | 
| 183 | 179, 182 | mpbird 257 | . . 3
⊢ (((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) ∧ 𝐼 ≠ ∅) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 184 | 119, 183 | pm2.61dane 3029 | . 2
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))) | 
| 185 | 87, 184 | jca 511 | 1
⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))) |