Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rrnequiv Structured version   Visualization version   GIF version

Theorem rrnequiv 32804
Description: The supremum metric on ℝ↑𝐼 is equivalent to the n metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
Hypotheses
Ref Expression
rrnequiv.y 𝑌 = ((ℂflds ℝ) ↑s 𝐼)
rrnequiv.d 𝐷 = (dist‘𝑌)
rrnequiv.1 𝑋 = (ℝ ↑𝑚 𝐼)
rrnequiv.i (𝜑𝐼 ∈ Fin)
Assertion
Ref Expression
rrnequiv ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn𝐼)𝐺) ∧ (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))))

Proof of Theorem rrnequiv
Dummy variables 𝑘 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rrnequiv.d . . . . . 6 𝐷 = (dist‘𝑌)
2 ovex 6577 . . . . . . . 8 (ℂflds ℝ) ∈ V
3 rrnequiv.i . . . . . . . . 9 (𝜑𝐼 ∈ Fin)
43adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐼 ∈ Fin)
5 rrnequiv.y . . . . . . . . 9 𝑌 = ((ℂflds ℝ) ↑s 𝐼)
6 reex 9906 . . . . . . . . . 10 ℝ ∈ V
7 eqid 2610 . . . . . . . . . . 11 (ℂflds ℝ) = (ℂflds ℝ)
8 eqid 2610 . . . . . . . . . . 11 (Scalar‘ℂfld) = (Scalar‘ℂfld)
97, 8resssca 15854 . . . . . . . . . 10 (ℝ ∈ V → (Scalar‘ℂfld) = (Scalar‘(ℂflds ℝ)))
106, 9ax-mp 5 . . . . . . . . 9 (Scalar‘ℂfld) = (Scalar‘(ℂflds ℝ))
115, 10pwsval 15969 . . . . . . . 8 (((ℂflds ℝ) ∈ V ∧ 𝐼 ∈ Fin) → 𝑌 = ((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
122, 4, 11sylancr 694 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝑌 = ((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
1312fveq2d 6107 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (dist‘𝑌) = (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
141, 13syl5eq 2656 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐷 = (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
1514oveqd 6566 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) = (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))𝐺))
16 fconstmpt 5085 . . . . . 6 (𝐼 × {(ℂflds ℝ)}) = (𝑘𝐼 ↦ (ℂflds ℝ))
1716oveq2i 6560 . . . . 5 ((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})) = ((Scalar‘ℂfld)Xs(𝑘𝐼 ↦ (ℂflds ℝ)))
18 eqid 2610 . . . . 5 (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))) = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
19 fvex 6113 . . . . . 6 (Scalar‘ℂfld) ∈ V
2019a1i 11 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (Scalar‘ℂfld) ∈ V)
212a1i 11 . . . . . 6 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → (ℂflds ℝ) ∈ V)
2221ralrimiva 2949 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 (ℂflds ℝ) ∈ V)
23 simprl 790 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹𝑋)
24 rrnequiv.1 . . . . . . 7 𝑋 = (ℝ ↑𝑚 𝐼)
25 ax-resscn 9872 . . . . . . . . . . 11 ℝ ⊆ ℂ
26 cnfldbas 19571 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
277, 26ressbas2 15758 . . . . . . . . . . 11 (ℝ ⊆ ℂ → ℝ = (Base‘(ℂflds ℝ)))
2825, 27ax-mp 5 . . . . . . . . . 10 ℝ = (Base‘(ℂflds ℝ))
295, 28pwsbas 15970 . . . . . . . . 9 (((ℂflds ℝ) ∈ V ∧ 𝐼 ∈ Fin) → (ℝ ↑𝑚 𝐼) = (Base‘𝑌))
302, 4, 29sylancr 694 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ℝ ↑𝑚 𝐼) = (Base‘𝑌))
3112fveq2d 6107 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (Base‘𝑌) = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
3230, 31eqtrd 2644 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ℝ ↑𝑚 𝐼) = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
3324, 32syl5eq 2656 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝑋 = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
3423, 33eleqtrd 2690 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹 ∈ (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
35 simprr 792 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺𝑋)
3635, 33eleqtrd 2690 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺 ∈ (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
37 cnfldds 19577 . . . . . . . 8 (abs ∘ − ) = (dist‘ℂfld)
387, 37ressds 15896 . . . . . . 7 (ℝ ∈ V → (abs ∘ − ) = (dist‘(ℂflds ℝ)))
396, 38ax-mp 5 . . . . . 6 (abs ∘ − ) = (dist‘(ℂflds ℝ))
4039reseq1i 5313 . . . . 5 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((dist‘(ℂflds ℝ)) ↾ (ℝ × ℝ))
41 eqid 2610 . . . . 5 (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))) = (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
4217, 18, 20, 4, 22, 34, 36, 28, 40, 41prdsdsval3 15968 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))𝐺) = sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
4315, 42eqtrd 2644 . . 3 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) = sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
44 eqid 2610 . . . . . . . . . 10 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
4524, 44rrndstprj1 32799 . . . . . . . . 9 (((𝐼 ∈ Fin ∧ 𝑘𝐼) ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
4645an32s 842 . . . . . . . 8 (((𝐼 ∈ Fin ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
473, 46sylanl1 680 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
4847ralrimiva 2949 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
49 ovex 6577 . . . . . . . 8 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V
5049rgenw 2908 . . . . . . 7 𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V
51 eqid 2610 . . . . . . . 8 (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) = (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))
52 breq1 4586 . . . . . . . 8 (𝑧 = ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) → (𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺)))
5351, 52ralrnmpt 6276 . . . . . . 7 (∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V → (∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺)))
5450, 53ax-mp 5 . . . . . 6 (∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
5548, 54sylibr 223 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺))
5624rrnmet 32798 . . . . . . . . 9 (𝐼 ∈ Fin → (ℝn𝐼) ∈ (Met‘𝑋))
574, 56syl 17 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ℝn𝐼) ∈ (Met‘𝑋))
58 metge0 21960 . . . . . . . 8 (((ℝn𝐼) ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → 0 ≤ (𝐹(ℝn𝐼)𝐺))
5957, 23, 35, 58syl3anc 1318 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (𝐹(ℝn𝐼)𝐺))
60 elsni 4142 . . . . . . . 8 (𝑧 ∈ {0} → 𝑧 = 0)
6160breq1d 4593 . . . . . . 7 (𝑧 ∈ {0} → (𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ 0 ≤ (𝐹(ℝn𝐼)𝐺)))
6259, 61syl5ibrcom 236 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝑧 ∈ {0} → 𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
6362ralrimiv 2948 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn𝐼)𝐺))
64 ralunb 3756 . . . . 5 (∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ (∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ∧ ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
6555, 63, 64sylanbrc 695 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺))
6617, 18, 20, 4, 22, 28, 34prdsbascl 15966 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 (𝐹𝑘) ∈ ℝ)
6766r19.21bi 2916 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → (𝐹𝑘) ∈ ℝ)
6817, 18, 20, 4, 22, 28, 36prdsbascl 15966 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 (𝐺𝑘) ∈ ℝ)
6968r19.21bi 2916 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → (𝐺𝑘) ∈ ℝ)
7044remet 22401 . . . . . . . . . . 11 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ)
71 metcl 21947 . . . . . . . . . . 11 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ) ∧ (𝐹𝑘) ∈ ℝ ∧ (𝐺𝑘) ∈ ℝ) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
7270, 71mp3an1 1403 . . . . . . . . . 10 (((𝐹𝑘) ∈ ℝ ∧ (𝐺𝑘) ∈ ℝ) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
7367, 69, 72syl2anc 691 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
7473, 51fmptd 6292 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))):𝐼⟶ℝ)
75 frn 5966 . . . . . . . 8 ((𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))):𝐼⟶ℝ → ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ ℝ)
7674, 75syl 17 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ ℝ)
77 ressxr 9962 . . . . . . 7 ℝ ⊆ ℝ*
7876, 77syl6ss 3580 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ ℝ*)
79 0xr 9965 . . . . . . . 8 0 ∈ ℝ*
8079a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ∈ ℝ*)
8180snssd 4281 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → {0} ⊆ ℝ*)
8278, 81unssd 3751 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ*)
83 metcl 21947 . . . . . . 7 (((ℝn𝐼) ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ)
8457, 23, 35, 83syl3anc 1318 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ)
8577, 84sseldi 3566 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ*)
86 supxrleub 12028 . . . . 5 (((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ* ∧ (𝐹(ℝn𝐼)𝐺) ∈ ℝ*) → (sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ) ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
8782, 85, 86syl2anc 691 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ) ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
8865, 87mpbird 246 . . 3 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ) ≤ (𝐹(ℝn𝐼)𝐺))
8943, 88eqbrtrd 4605 . 2 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) ≤ (𝐹(ℝn𝐼)𝐺))
90 rzal 4025 . . . . . . 7 (𝐼 = ∅ → ∀𝑘𝐼 (𝐹𝑘) = (𝐺𝑘))
9123, 24syl6eleq 2698 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹 ∈ (ℝ ↑𝑚 𝐼))
92 elmapi 7765 . . . . . . . . 9 (𝐹 ∈ (ℝ ↑𝑚 𝐼) → 𝐹:𝐼⟶ℝ)
93 ffn 5958 . . . . . . . . 9 (𝐹:𝐼⟶ℝ → 𝐹 Fn 𝐼)
9491, 92, 933syl 18 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹 Fn 𝐼)
9535, 24syl6eleq 2698 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺 ∈ (ℝ ↑𝑚 𝐼))
96 elmapi 7765 . . . . . . . . 9 (𝐺 ∈ (ℝ ↑𝑚 𝐼) → 𝐺:𝐼⟶ℝ)
97 ffn 5958 . . . . . . . . 9 (𝐺:𝐼⟶ℝ → 𝐺 Fn 𝐼)
9895, 96, 973syl 18 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺 Fn 𝐼)
99 eqfnfv 6219 . . . . . . . 8 ((𝐹 Fn 𝐼𝐺 Fn 𝐼) → (𝐹 = 𝐺 ↔ ∀𝑘𝐼 (𝐹𝑘) = (𝐺𝑘)))
10094, 98, 99syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹 = 𝐺 ↔ ∀𝑘𝐼 (𝐹𝑘) = (𝐺𝑘)))
10190, 100syl5ibr 235 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐼 = ∅ → 𝐹 = 𝐺))
102101imp 444 . . . . 5 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → 𝐹 = 𝐺)
103102oveq1d 6564 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn𝐼)𝐺) = (𝐺(ℝn𝐼)𝐺))
104 met0 21958 . . . . . . 7 (((ℝn𝐼) ∈ (Met‘𝑋) ∧ 𝐺𝑋) → (𝐺(ℝn𝐼)𝐺) = 0)
10557, 35, 104syl2anc 691 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐺(ℝn𝐼)𝐺) = 0)
106 hashcl 13009 . . . . . . . . . 10 (𝐼 ∈ Fin → (#‘𝐼) ∈ ℕ0)
1074, 106syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (#‘𝐼) ∈ ℕ0)
108107nn0red 11229 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (#‘𝐼) ∈ ℝ)
109107nn0ge0d 11231 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (#‘𝐼))
110108, 109resqrtcld 14004 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (√‘(#‘𝐼)) ∈ ℝ)
1115, 1, 24repwsmet 32803 . . . . . . . . 9 (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋))
1124, 111syl 17 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐷 ∈ (Met‘𝑋))
113 metcl 21947 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → (𝐹𝐷𝐺) ∈ ℝ)
114112, 23, 35, 113syl3anc 1318 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) ∈ ℝ)
115108, 109sqrtge0d 14007 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (√‘(#‘𝐼)))
116 metge0 21960 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → 0 ≤ (𝐹𝐷𝐺))
117112, 23, 35, 116syl3anc 1318 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (𝐹𝐷𝐺))
118110, 114, 115, 117mulge0d 10483 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
119105, 118eqbrtrd 4605 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐺(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
120119adantr 480 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → (𝐺(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
121103, 120eqbrtrd 4605 . . 3 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
12284adantr 480 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ)
123110, 114remulcld 9949 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ)
124123adantr 480 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ)
125 rpre 11715 . . . . . . . . 9 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
126125ad2antll 761 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ)
127124, 126readdcld 9948 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟) ∈ ℝ)
1284adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
129 simprl 790 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ≠ ∅)
130 eldifsn 4260 . . . . . . . . . 10 (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
131128, 129, 130sylanbrc 695 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ (Fin ∖ {∅}))
13223adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐹𝑋)
13335adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐺𝑋)
134114adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℝ)
135 simprr 792 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ+)
136 hashnncl 13018 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ Fin → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
137128, 136syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
138129, 137mpbird 246 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (#‘𝐼) ∈ ℕ)
139138nnrpd 11746 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (#‘𝐼) ∈ ℝ+)
140139rpsqrtcld 13998 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(#‘𝐼)) ∈ ℝ+)
141135, 140rpdivcld 11765 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(#‘𝐼))) ∈ ℝ+)
142141rpred 11748 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(#‘𝐼))) ∈ ℝ)
143134, 142readdcld 9948 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ)
144 0red 9920 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ∈ ℝ)
145117adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ≤ (𝐹𝐷𝐺))
146134, 141ltaddrpd 11781 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))
147144, 134, 143, 145, 146lelttrd 10074 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))
148143, 147elrpd 11745 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ+)
14973adantlr 747 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
150134adantr 480 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (𝐹𝐷𝐺) ∈ ℝ)
151143adantr 480 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ)
15282ad2antrr 758 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ*)
153 ssun1 3738 . . . . . . . . . . . . . 14 ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})
154 simpr 476 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → 𝑘𝐼)
15551elrnmpt1 5295 . . . . . . . . . . . . . . 15 ((𝑘𝐼 ∧ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))))
156154, 49, 155sylancl 693 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))))
157153, 156sseldi 3566 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}))
158 supxrub 12026 . . . . . . . . . . . . 13 (((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ* ∧ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
159152, 157, 158syl2anc 691 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
16043ad2antrr 758 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (𝐹𝐷𝐺) = sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
161159, 160breqtrrd 4611 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹𝐷𝐺))
162146adantr 480 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))
163149, 150, 151, 161, 162lelttrd 10074 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))
164163ralrimiva 2949 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))
16524, 44rrndstprj2 32800 . . . . . . . . 9 (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹𝑋𝐺𝑋) ∧ (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) ∈ ℝ+ ∧ ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))))) → (𝐹(ℝn𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼))))
166131, 132, 133, 148, 164, 165syl32anc 1326 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼))))
167134recnd 9947 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℂ)
168142recnd 9947 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(#‘𝐼))) ∈ ℂ)
169110adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(#‘𝐼)) ∈ ℝ)
170169recnd 9947 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(#‘𝐼)) ∈ ℂ)
171167, 168, 170adddird 9944 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼))) = (((𝐹𝐷𝐺) · (√‘(#‘𝐼))) + ((𝑟 / (√‘(#‘𝐼))) · (√‘(#‘𝐼)))))
172167, 170mulcomd 9940 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) · (√‘(#‘𝐼))) = ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
173126recnd 9947 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℂ)
174140rpne0d 11753 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(#‘𝐼)) ≠ 0)
175173, 170, 174divcan1d 10681 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝑟 / (√‘(#‘𝐼))) · (√‘(#‘𝐼))) = 𝑟)
176172, 175oveq12d 6567 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) · (√‘(#‘𝐼))) + ((𝑟 / (√‘(#‘𝐼))) · (√‘(#‘𝐼)))) = (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
177171, 176eqtrd 2644 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(#‘𝐼)))) · (√‘(#‘𝐼))) = (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
178166, 177breqtrd 4609 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) < (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
179122, 127, 178ltled 10064 . . . . . 6 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
180179anassrs 678 . . . . 5 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
181180ralrimiva 2949 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) → ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
182 alrple 11911 . . . . . 6 (((𝐹(ℝn𝐼)𝐺) ∈ ℝ ∧ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) → ((𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)))
18384, 123, 182syl2anc 691 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)))
184183adantr 480 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) → ((𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(#‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)))
185181, 184mpbird 246 . . 3 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) → (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
186121, 185pm2.61dane 2869 . 2 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺)))
18789, 186jca 553 1 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn𝐼)𝐺) ∧ (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(#‘𝐼)) · (𝐹𝐷𝐺))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wne 2780  wral 2896  Vcvv 3173  cdif 3537  cun 3538  wss 3540  c0 3874  {csn 4125   class class class wbr 4583  cmpt 4643   × cxp 5036  ran crn 5039  cres 5040  ccom 5042   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  𝑚 cmap 7744  Fincfn 7841  supcsup 8229  cc 9813  cr 9814  0cc0 9815   + caddc 9818   · cmul 9820  *cxr 9952   < clt 9953  cle 9954  cmin 10145   / cdiv 10563  cn 10897  0cn0 11169  +crp 11708  #chash 12979  csqrt 13821  abscabs 13822  Basecbs 15695  s cress 15696  Scalarcsca 15771  distcds 15777  Xscprds 15929  s cpws 15930  Metcme 19553  fldccnfld 19567  ncrrn 32794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-prds 15931  df-pws 15933  df-xmet 19560  df-met 19561  df-cnfld 19568  df-rrn 32795
This theorem is referenced by:  rrntotbnd  32805
  Copyright terms: Public domain W3C validator