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 33866
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 6793 . . . . . . . 8 (ℂflds ℝ) ∈ V
3 rrnequiv.i . . . . . . . . 9 (𝜑𝐼 ∈ Fin)
43adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐼 ∈ Fin)
5 rrnequiv.y . . . . . . . . 9 𝑌 = ((ℂflds ℝ) ↑s 𝐼)
6 reex 10140 . . . . . . . . . 10 ℝ ∈ V
7 eqid 2724 . . . . . . . . . . 11 (ℂflds ℝ) = (ℂflds ℝ)
8 eqid 2724 . . . . . . . . . . 11 (Scalar‘ℂfld) = (Scalar‘ℂfld)
97, 8resssca 16154 . . . . . . . . . 10 (ℝ ∈ V → (Scalar‘ℂfld) = (Scalar‘(ℂflds ℝ)))
106, 9ax-mp 5 . . . . . . . . 9 (Scalar‘ℂfld) = (Scalar‘(ℂflds ℝ))
115, 10pwsval 16269 . . . . . . . 8 (((ℂflds ℝ) ∈ V ∧ 𝐼 ∈ Fin) → 𝑌 = ((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
122, 4, 11sylancr 698 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝑌 = ((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
1312fveq2d 6308 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (dist‘𝑌) = (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
141, 13syl5eq 2770 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐷 = (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
1514oveqd 6782 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) = (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))𝐺))
16 fconstmpt 5272 . . . . . 6 (𝐼 × {(ℂflds ℝ)}) = (𝑘𝐼 ↦ (ℂflds ℝ))
1716oveq2i 6776 . . . . 5 ((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})) = ((Scalar‘ℂfld)Xs(𝑘𝐼 ↦ (ℂflds ℝ)))
18 eqid 2724 . . . . 5 (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))) = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
19 fvexd 6316 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (Scalar‘ℂfld) ∈ V)
202a1i 11 . . . . . 6 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → (ℂflds ℝ) ∈ V)
2120ralrimiva 3068 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 (ℂflds ℝ) ∈ V)
22 simprl 811 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹𝑋)
23 rrnequiv.1 . . . . . . 7 𝑋 = (ℝ ↑𝑚 𝐼)
24 ax-resscn 10106 . . . . . . . . . . 11 ℝ ⊆ ℂ
25 cnfldbas 19873 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
267, 25ressbas2 16054 . . . . . . . . . . 11 (ℝ ⊆ ℂ → ℝ = (Base‘(ℂflds ℝ)))
2724, 26ax-mp 5 . . . . . . . . . 10 ℝ = (Base‘(ℂflds ℝ))
285, 27pwsbas 16270 . . . . . . . . 9 (((ℂflds ℝ) ∈ V ∧ 𝐼 ∈ Fin) → (ℝ ↑𝑚 𝐼) = (Base‘𝑌))
292, 4, 28sylancr 698 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ℝ ↑𝑚 𝐼) = (Base‘𝑌))
3012fveq2d 6308 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (Base‘𝑌) = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
3129, 30eqtrd 2758 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ℝ ↑𝑚 𝐼) = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
3223, 31syl5eq 2770 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝑋 = (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
3322, 32eleqtrd 2805 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹 ∈ (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
34 simprr 813 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺𝑋)
3534, 32eleqtrd 2805 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺 ∈ (Base‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))))
36 cnfldds 19879 . . . . . . . 8 (abs ∘ − ) = (dist‘ℂfld)
377, 36ressds 16196 . . . . . . 7 (ℝ ∈ V → (abs ∘ − ) = (dist‘(ℂflds ℝ)))
386, 37ax-mp 5 . . . . . 6 (abs ∘ − ) = (dist‘(ℂflds ℝ))
3938reseq1i 5499 . . . . 5 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((dist‘(ℂflds ℝ)) ↾ (ℝ × ℝ))
40 eqid 2724 . . . . 5 (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)}))) = (dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))
4117, 18, 19, 4, 21, 33, 35, 27, 39, 40prdsdsval3 16268 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(dist‘((Scalar‘ℂfld)Xs(𝐼 × {(ℂflds ℝ)})))𝐺) = sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
4215, 41eqtrd 2758 . . 3 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) = sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
43 eqid 2724 . . . . . . . . . 10 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
4423, 43rrndstprj1 33861 . . . . . . . . 9 (((𝐼 ∈ Fin ∧ 𝑘𝐼) ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
4544an32s 881 . . . . . . . 8 (((𝐼 ∈ Fin ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
463, 45sylanl1 685 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
4746ralrimiva 3068 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
48 ovex 6793 . . . . . . . 8 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V
4948rgenw 3026 . . . . . . 7 𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V
50 eqid 2724 . . . . . . . 8 (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) = (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))
51 breq1 4763 . . . . . . . 8 (𝑧 = ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) → (𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺)))
5250, 51ralrnmpt 6483 . . . . . . 7 (∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V → (∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺)))
5349, 52ax-mp 5 . . . . . 6 (∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹(ℝn𝐼)𝐺))
5447, 53sylibr 224 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺))
5523rrnmet 33860 . . . . . . . . 9 (𝐼 ∈ Fin → (ℝn𝐼) ∈ (Met‘𝑋))
564, 55syl 17 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ℝn𝐼) ∈ (Met‘𝑋))
57 metge0 22272 . . . . . . . 8 (((ℝn𝐼) ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → 0 ≤ (𝐹(ℝn𝐼)𝐺))
5856, 22, 34, 57syl3anc 1439 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (𝐹(ℝn𝐼)𝐺))
59 elsni 4302 . . . . . . . 8 (𝑧 ∈ {0} → 𝑧 = 0)
6059breq1d 4770 . . . . . . 7 (𝑧 ∈ {0} → (𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ 0 ≤ (𝐹(ℝn𝐼)𝐺)))
6158, 60syl5ibrcom 237 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝑧 ∈ {0} → 𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
6261ralrimiv 3067 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn𝐼)𝐺))
63 ralunb 3902 . . . . 5 (∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ↔ (∀𝑧 ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)))𝑧 ≤ (𝐹(ℝn𝐼)𝐺) ∧ ∀𝑧 ∈ {0}𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
6454, 62, 63sylanbrc 701 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺))
6517, 18, 19, 4, 21, 27, 33prdsbascl 16266 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 (𝐹𝑘) ∈ ℝ)
6665r19.21bi 3034 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → (𝐹𝑘) ∈ ℝ)
6717, 18, 19, 4, 21, 27, 35prdsbascl 16266 . . . . . . . . . . 11 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ∀𝑘𝐼 (𝐺𝑘) ∈ ℝ)
6867r19.21bi 3034 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → (𝐺𝑘) ∈ ℝ)
6943remet 22715 . . . . . . . . . . 11 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ)
70 metcl 22259 . . . . . . . . . . 11 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (Met‘ℝ) ∧ (𝐹𝑘) ∈ ℝ ∧ (𝐺𝑘) ∈ ℝ) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
7169, 70mp3an1 1524 . . . . . . . . . 10 (((𝐹𝑘) ∈ ℝ ∧ (𝐺𝑘) ∈ ℝ) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
7266, 68, 71syl2anc 696 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
7372, 50fmptd 6500 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))):𝐼⟶ℝ)
74 frn 6166 . . . . . . . 8 ((𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))):𝐼⟶ℝ → ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ ℝ)
7573, 74syl 17 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ ℝ)
76 ressxr 10196 . . . . . . 7 ℝ ⊆ ℝ*
7775, 76syl6ss 3721 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ ℝ*)
78 0xr 10199 . . . . . . . 8 0 ∈ ℝ*
7978a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ∈ ℝ*)
8079snssd 4448 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → {0} ⊆ ℝ*)
8177, 80unssd 3897 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ*)
82 metcl 22259 . . . . . . 7 (((ℝn𝐼) ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ)
8356, 22, 34, 82syl3anc 1439 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ)
8476, 83sseldi 3707 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ*)
85 supxrleub 12270 . . . . 5 (((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ* ∧ (𝐹(ℝn𝐼)𝐺) ∈ ℝ*) → (sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ) ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
8681, 84, 85syl2anc 696 . . . 4 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ) ≤ (𝐹(ℝn𝐼)𝐺) ↔ ∀𝑧 ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})𝑧 ≤ (𝐹(ℝn𝐼)𝐺)))
8764, 86mpbird 247 . . 3 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ) ≤ (𝐹(ℝn𝐼)𝐺))
8842, 87eqbrtrd 4782 . 2 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) ≤ (𝐹(ℝn𝐼)𝐺))
89 rzal 4181 . . . . . . 7 (𝐼 = ∅ → ∀𝑘𝐼 (𝐹𝑘) = (𝐺𝑘))
9022, 23syl6eleq 2813 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹 ∈ (ℝ ↑𝑚 𝐼))
91 elmapi 7996 . . . . . . . . 9 (𝐹 ∈ (ℝ ↑𝑚 𝐼) → 𝐹:𝐼⟶ℝ)
92 ffn 6158 . . . . . . . . 9 (𝐹:𝐼⟶ℝ → 𝐹 Fn 𝐼)
9390, 91, 923syl 18 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐹 Fn 𝐼)
9434, 23syl6eleq 2813 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺 ∈ (ℝ ↑𝑚 𝐼))
95 elmapi 7996 . . . . . . . . 9 (𝐺 ∈ (ℝ ↑𝑚 𝐼) → 𝐺:𝐼⟶ℝ)
96 ffn 6158 . . . . . . . . 9 (𝐺:𝐼⟶ℝ → 𝐺 Fn 𝐼)
9794, 95, 963syl 18 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐺 Fn 𝐼)
98 eqfnfv 6426 . . . . . . . 8 ((𝐹 Fn 𝐼𝐺 Fn 𝐼) → (𝐹 = 𝐺 ↔ ∀𝑘𝐼 (𝐹𝑘) = (𝐺𝑘)))
9993, 97, 98syl2anc 696 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹 = 𝐺 ↔ ∀𝑘𝐼 (𝐹𝑘) = (𝐺𝑘)))
10089, 99syl5ibr 236 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐼 = ∅ → 𝐹 = 𝐺))
101100imp 444 . . . . 5 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → 𝐹 = 𝐺)
102101oveq1d 6780 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn𝐼)𝐺) = (𝐺(ℝn𝐼)𝐺))
103 met0 22270 . . . . . . 7 (((ℝn𝐼) ∈ (Met‘𝑋) ∧ 𝐺𝑋) → (𝐺(ℝn𝐼)𝐺) = 0)
10456, 34, 103syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐺(ℝn𝐼)𝐺) = 0)
105 hashcl 13260 . . . . . . . . . 10 (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ0)
1064, 105syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (♯‘𝐼) ∈ ℕ0)
107106nn0red 11465 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (♯‘𝐼) ∈ ℝ)
108106nn0ge0d 11467 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (♯‘𝐼))
109107, 108resqrtcld 14276 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (√‘(♯‘𝐼)) ∈ ℝ)
1105, 1, 23repwsmet 33865 . . . . . . . . 9 (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋))
1114, 110syl 17 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 𝐷 ∈ (Met‘𝑋))
112 metcl 22259 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → (𝐹𝐷𝐺) ∈ ℝ)
113111, 22, 34, 112syl3anc 1439 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹𝐷𝐺) ∈ ℝ)
114107, 108sqrtge0d 14279 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (√‘(♯‘𝐼)))
115 metge0 22272 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐹𝑋𝐺𝑋) → 0 ≤ (𝐹𝐷𝐺))
116111, 22, 34, 115syl3anc 1439 . . . . . . 7 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ (𝐹𝐷𝐺))
117109, 113, 114, 116mulge0d 10717 . . . . . 6 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → 0 ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
118104, 117eqbrtrd 4782 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐺(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
119118adantr 472 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → (𝐺(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
120102, 119eqbrtrd 4782 . . 3 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 = ∅) → (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
12183adantr 472 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) ∈ ℝ)
122109, 113remulcld 10183 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ)
123122adantr 472 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ)
124 rpre 11953 . . . . . . . . 9 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
125124ad2antll 767 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ)
126123, 125readdcld 10182 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟) ∈ ℝ)
1274adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin)
128 simprl 811 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ≠ ∅)
129 eldifsn 4425 . . . . . . . . . 10 (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
130127, 128, 129sylanbrc 701 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ (Fin ∖ {∅}))
13122adantr 472 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐹𝑋)
13234adantr 472 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝐺𝑋)
133113adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℝ)
134 simprr 813 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ+)
135 hashnncl 13270 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ Fin → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
136127, 135syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
137128, 136mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (♯‘𝐼) ∈ ℕ)
138137nnrpd 11984 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (♯‘𝐼) ∈ ℝ+)
139138rpsqrtcld 14270 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(♯‘𝐼)) ∈ ℝ+)
140134, 139rpdivcld 12003 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(♯‘𝐼))) ∈ ℝ+)
141140rpred 11986 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(♯‘𝐼))) ∈ ℝ)
142133, 141readdcld 10182 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈ ℝ)
143 0red 10154 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ∈ ℝ)
144116adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 ≤ (𝐹𝐷𝐺))
145133, 140ltaddrpd 12019 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))
146143, 133, 142, 144, 145lelttrd 10308 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 0 < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))
147142, 146elrpd 11983 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈ ℝ+)
14872adantlr 753 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ℝ)
149133adantr 472 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (𝐹𝐷𝐺) ∈ ℝ)
150142adantr 472 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈ ℝ)
15181ad2antrr 764 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ*)
152 ssun1 3884 . . . . . . . . . . . . . 14 ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ⊆ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})
153 simpr 479 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → 𝑘𝐼)
15450elrnmpt1 5481 . . . . . . . . . . . . . . 15 ((𝑘𝐼 ∧ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ V) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))))
155153, 48, 154sylancl 697 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))))
156152, 155sseldi 3707 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}))
157 supxrub 12268 . . . . . . . . . . . . 13 (((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}) ⊆ ℝ* ∧ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ∈ (ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0})) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
158151, 156, 157syl2anc 696 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
15942ad2antrr 764 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (𝐹𝐷𝐺) = sup((ran (𝑘𝐼 ↦ ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘))) ∪ {0}), ℝ*, < ))
160158, 159breqtrrd 4788 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) ≤ (𝐹𝐷𝐺))
161145adantr 472 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → (𝐹𝐷𝐺) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))
162148, 149, 150, 160, 161lelttrd 10308 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) ∧ 𝑘𝐼) → ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))
163162ralrimiva 3068 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))
16423, 43rrndstprj2 33862 . . . . . . . . 9 (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹𝑋𝐺𝑋) ∧ (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) ∈ ℝ+ ∧ ∀𝑘𝐼 ((𝐹𝑘)((abs ∘ − ) ↾ (ℝ × ℝ))(𝐺𝑘)) < ((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))))) → (𝐹(ℝn𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) · (√‘(♯‘𝐼))))
165130, 131, 132, 147, 163, 164syl32anc 1447 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) < (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) · (√‘(♯‘𝐼))))
166133recnd 10181 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹𝐷𝐺) ∈ ℂ)
167141recnd 10181 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝑟 / (√‘(♯‘𝐼))) ∈ ℂ)
168109adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(♯‘𝐼)) ∈ ℝ)
169168recnd 10181 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(♯‘𝐼)) ∈ ℂ)
170166, 167, 169adddird 10178 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) · (√‘(♯‘𝐼))) = (((𝐹𝐷𝐺) · (√‘(♯‘𝐼))) + ((𝑟 / (√‘(♯‘𝐼))) · (√‘(♯‘𝐼)))))
171166, 169mulcomd 10174 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝐹𝐷𝐺) · (√‘(♯‘𝐼))) = ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
172125recnd 10181 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈ ℂ)
173139rpne0d 11991 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (√‘(♯‘𝐼)) ≠ 0)
174172, 169, 173divcan1d 10915 . . . . . . . . . 10 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → ((𝑟 / (√‘(♯‘𝐼))) · (√‘(♯‘𝐼))) = 𝑟)
175171, 174oveq12d 6783 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) · (√‘(♯‘𝐼))) + ((𝑟 / (√‘(♯‘𝐼))) · (√‘(♯‘𝐼)))) = (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
176170, 175eqtrd 2758 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (((𝐹𝐷𝐺) + (𝑟 / (√‘(♯‘𝐼)))) · (√‘(♯‘𝐼))) = (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
177165, 176breqtrd 4786 . . . . . . 7 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) < (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
178121, 126, 177ltled 10298 . . . . . 6 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ (𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+)) → (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
179178anassrs 683 . . . . 5 ((((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) ∧ 𝑟 ∈ ℝ+) → (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
180179ralrimiva 3068 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) → ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟))
181 alrple 12151 . . . . . 6 (((𝐹(ℝn𝐼)𝐺) ∈ ℝ ∧ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ∈ ℝ) → ((𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)))
18283, 122, 181syl2anc 696 . . . . 5 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)))
183182adantr 472 . . . 4 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) → ((𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) ↔ ∀𝑟 ∈ ℝ+ (𝐹(ℝn𝐼)𝐺) ≤ (((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)) + 𝑟)))
184180, 183mpbird 247 . . 3 (((𝜑 ∧ (𝐹𝑋𝐺𝑋)) ∧ 𝐼 ≠ ∅) → (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
185120, 184pm2.61dane 2983 . 2 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺)))
18688, 185jca 555 1 ((𝜑 ∧ (𝐹𝑋𝐺𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn𝐼)𝐺) ∧ (𝐹(ℝn𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wcel 2103  wne 2896  wral 3014  Vcvv 3304  cdif 3677  cun 3678  wss 3680  c0 4023  {csn 4285   class class class wbr 4760  cmpt 4837   × cxp 5216  ran crn 5219  cres 5220  ccom 5222   Fn wfn 5996  wf 5997  cfv 6001  (class class class)co 6765  𝑚 cmap 7974  Fincfn 8072  supcsup 8462  cc 10047  cr 10048  0cc0 10049   + caddc 10052   · cmul 10054  *cxr 10186   < clt 10187  cle 10188  cmin 10379   / cdiv 10797  cn 11133  0cn0 11405  +crp 11946  chash 13232  csqrt 14093  abscabs 14094  Basecbs 15980  s cress 15981  Scalarcsca 16067  distcds 16073  Xscprds 16229  s cpws 16230  Metcme 19855  fldccnfld 19869  ncrrn 33856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-inf2 8651  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-se 5178  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-isom 6010  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-map 7976  df-ixp 8026  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-inf 8465  df-oi 8531  df-card 8878  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-q 11903  df-rp 11947  df-xneg 12060  df-xadd 12061  df-xmul 12062  df-ico 12295  df-icc 12296  df-fz 12441  df-fzo 12581  df-seq 12917  df-exp 12976  df-hash 13233  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-clim 14339  df-sum 14537  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-starv 16079  df-sca 16080  df-vsca 16081  df-ip 16082  df-tset 16083  df-ple 16084  df-ds 16087  df-unif 16088  df-hom 16089  df-cco 16090  df-prds 16231  df-pws 16233  df-xmet 19862  df-met 19863  df-cnfld 19870  df-rrn 33857
This theorem is referenced by:  rrntotbnd  33867
  Copyright terms: Public domain W3C validator