Metamath Proof Explorer

Theorem rrnequiv

Description: The supremum metric on RR ^ I is equivalent to the Rn metric. (Contributed by Jeff Madsen, 15-Sep-2015)

Ref Expression
Hypotheses rrnequiv.y ⊢ 𝑌 = ( ( ℂfld ↾s ℝ ) ↑s 𝐼 )
rrnequiv.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
rrnequiv.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
rrnequiv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
Assertion rrnequiv ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 𝐷 𝐺 ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∧ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 rrnequiv.y ⊢ 𝑌 = ( ( ℂfld ↾s ℝ ) ↑s 𝐼 )
2 rrnequiv.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
3 rrnequiv.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
4 rrnequiv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
5 ovex ⊢ ( ℂfld ↾s ℝ ) ∈ V
6 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐼 ∈ Fin )
7 reex ⊢ ℝ ∈ V
8 eqid ⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ℝ )
9 eqid ⊢ ( Scalar ‘ ℂfld ) = ( Scalar ‘ ℂfld )
10 8 9 resssca ⊢ ( ℝ ∈ V → ( Scalar ‘ ℂfld ) = ( Scalar ‘ ( ℂfld ↾s ℝ ) ) )
11 7 10 ax-mp ⊢ ( Scalar ‘ ℂfld ) = ( Scalar ‘ ( ℂfld ↾s ℝ ) )
12 1 11 pwsval ⊢ ( ( ( ℂfld ↾s ℝ ) ∈ V ∧ 𝐼 ∈ Fin ) → 𝑌 = ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
13 5 6 12 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝑌 = ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
14 13 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( dist ‘ 𝑌 ) = ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
15 2 14 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐷 = ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
16 15 oveqd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 𝐷 𝐺 ) = ( 𝐹 ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) 𝐺 ) )
17 fconstmpt ⊢ ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) = ( 𝑘 ∈ 𝐼 ↦ ( ℂfld ↾s ℝ ) )
18 17 oveq2i ⊢ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) = ( ( Scalar ‘ ℂfld ) Xs ( 𝑘 ∈ 𝐼 ↦ ( ℂfld ↾s ℝ ) ) )
19 eqid ⊢ ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
20 fvexd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( Scalar ‘ ℂfld ) ∈ V )
21 5 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ℂfld ↾s ℝ ) ∈ V )
22 21 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑘 ∈ 𝐼 ( ℂfld ↾s ℝ ) ∈ V )
23 simprl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ 𝑋 )
24 ax-resscn ⊢ ℝ ⊆ ℂ
25 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
26 8 25 ressbas2 ⊢ ( ℝ ⊆ ℂ → ℝ = ( Base ‘ ( ℂfld ↾s ℝ ) ) )
27 24 26 ax-mp ⊢ ℝ = ( Base ‘ ( ℂfld ↾s ℝ ) )
28 1 27 pwsbas ⊢ ( ( ( ℂfld ↾s ℝ ) ∈ V ∧ 𝐼 ∈ Fin ) → ( ℝ ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )
29 5 6 28 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ℝ ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )
30 13 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
31 29 30 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ℝ ↑m 𝐼 ) = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
32 3 31 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝑋 = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
33 23 32 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
34 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ 𝑋 )
35 34 32 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
36 cnfldds ⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
37 8 36 ressds ⊢ ( ℝ ∈ V → ( abs ∘ − ) = ( dist ‘ ( ℂfld ↾s ℝ ) ) )
38 7 37 ax-mp ⊢ ( abs ∘ − ) = ( dist ‘ ( ℂfld ↾s ℝ ) )
39 38 reseq1i ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ( ℂfld ↾s ℝ ) ) ↾ ( ℝ × ℝ ) )
40 eqid ⊢ ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) = ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
41 18 19 20 6 22 33 35 27 39 40 prdsdsval3 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) 𝐺 ) = sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
42 16 41 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
43 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
44 3 43 rrndstprj1 ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
45 44 an32s ⊢ ( ( ( 𝐼 ∈ Fin ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
46 4 45 sylanl1 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
47 46 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
48 ovex ⊢ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ V
49 48 rgenw ⊢ ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ V
50 eqid ⊢ ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) )
51 breq1 ⊢ ( 𝑧 = ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) → ( 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
52 50 51 ralrnmptw ⊢ ( ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
53 49 52 ax-mp ⊢ ( ∀ 𝑧 ∈ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
54 47 53 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑧 ∈ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
55 3 rrnmet ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )
56 6 55 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )
57 metge0 ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 0 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
58 56 23 34 57 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
59 elsni ⊢ ( 𝑧 ∈ { 0 } → 𝑧 = 0 )
60 59 breq1d ⊢ ( 𝑧 ∈ { 0 } → ( 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ 0 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
61 58 60 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝑧 ∈ { 0 } → 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
62 61 ralrimiv ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑧 ∈ { 0 } 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
63 ralunb ⊢ ( ∀ 𝑧 ∈ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ ( ∀ 𝑧 ∈ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∧ ∀ 𝑧 ∈ { 0 } 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
64 54 62 63 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑧 ∈ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
65 18 19 20 6 22 27 33 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑘 ∈ 𝐼 ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
66 65 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
67 18 19 20 6 22 27 35 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ∀ 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
68 67 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
69 43 remet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ )
70 metcl ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑘 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
71 69 70 mp3an1 ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑘 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
72 66 68 71 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
73 72 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) : 𝐼 ⟶ ℝ )
74 73 frnd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ⊆ ℝ )
75 ressxr ⊢ ℝ ⊆ ℝ*
76 74 75 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ⊆ ℝ* )
77 0xr ⊢ 0 ∈ ℝ*
78 77 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ∈ ℝ* )
79 78 snssd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → { 0 } ⊆ ℝ* )
80 76 79 unssd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
81 metcl ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∈ ℝ )
82 56 23 34 81 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∈ ℝ )
83 75 82 sselid ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∈ ℝ* )
84 supxrleub ⊢ ( ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∈ ℝ* ) → ( sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ ∀ 𝑧 ∈ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
85 80 83 84 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ↔ ∀ 𝑧 ∈ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ) )
86 64 85 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
87 42 86 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 𝐷 𝐺 ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) )
88 rzal ⊢ ( 𝐼 = ∅ → ∀ 𝑘 ∈ 𝐼 ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
89 23 3 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
90 elmapi ⊢ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℝ )
91 ffn ⊢ ( 𝐹 : 𝐼 ⟶ ℝ → 𝐹 Fn 𝐼 )
92 89 90 91 3syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐹 Fn 𝐼 )
93 34 3 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
94 elmapi ⊢ ( 𝐺 ∈ ( ℝ ↑m 𝐼 ) → 𝐺 : 𝐼 ⟶ ℝ )
95 ffn ⊢ ( 𝐺 : 𝐼 ⟶ ℝ → 𝐺 Fn 𝐼 )
96 93 94 95 3syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐺 Fn 𝐼 )
97 eqfnfv ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝐺 Fn 𝐼 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
98 92 96 97 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
99 88 98 syl5ibr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐼 = ∅ → 𝐹 = 𝐺 ) )
100 99 imp ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 = ∅ ) → 𝐹 = 𝐺 )
101 100 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 = ∅ ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( 𝐺 ( ℝn ‘ 𝐼 ) 𝐺 ) )
102 met0 ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ 𝐺 ∈ 𝑋 ) → ( 𝐺 ( ℝn ‘ 𝐼 ) 𝐺 ) = 0 )
103 56 34 102 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 ( ℝn ‘ 𝐼 ) 𝐺 ) = 0 )
104 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
105 6 104 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
106 105 nn0red ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
107 105 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( ♯ ‘ 𝐼 ) )
108 106 107 resqrtcld ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
109 1 2 3 repwsmet ⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ 𝑋 ) )
110 6 109 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
111 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) ∈ ℝ )
112 110 23 34 111 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 𝐷 𝐺 ) ∈ ℝ )
113 106 107 sqrtge0d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
114 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → 0 ≤ ( 𝐹 𝐷 𝐺 ) )
115 110 23 34 114 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( 𝐹 𝐷 𝐺 ) )
116 108 112 113 115 mulge0d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 0 ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
117 103 116 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐺 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
118 117 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 = ∅ ) → ( 𝐺 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
119 101 118 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 = ∅ ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
120 82 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∈ ℝ )
121 108 112 remulcld ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ∈ ℝ )
122 121 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ∈ ℝ )
123 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
124 123 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ )
125 122 124 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) ∈ ℝ )
126 6 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝐼 ∈ Fin )
127 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝐼 ≠ ∅ )
128 eldifsn ⊢ ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ↔ ( 𝐼 ∈ Fin ∧ 𝐼 ≠ ∅ ) )
129 126 127 128 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝐼 ∈ ( Fin ∖ { ∅ } ) )
130 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝐹 ∈ 𝑋 )
131 34 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝐺 ∈ 𝑋 )
132 112 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 𝐷 𝐺 ) ∈ ℝ )
133 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ+ )
134 hashnncl ⊢ ( 𝐼 ∈ Fin → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
135 126 134 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
136 127 135 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ )
137 136 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
138 137 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ+ )
139 133 138 rpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ+ )
140 139 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
141 132 140 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
142 0red ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 0 ∈ ℝ )
143 115 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 0 ≤ ( 𝐹 𝐷 𝐺 ) )
144 132 139 ltaddrpd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 𝐷 𝐺 ) < ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
145 142 132 141 143 144 lelttrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 0 < ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
146 141 145 elrpd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ+ )
147 72 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
148 132 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 𝐷 𝐺 ) ∈ ℝ )
149 141 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
150 80 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
151 ssun1 ⊢ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ⊆ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } )
152 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
153 50 elrnmpt1 ⊢ ( ( 𝑘 ∈ 𝐼 ∧ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ V ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
154 152 48 153 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
155 151 154 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) )
156 supxrub ⊢ ( ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
157 150 155 156 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
158 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
159 157 158 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐹 𝐷 𝐺 ) )
160 144 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 𝐷 𝐺 ) < ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
161 147 148 149 159 160 lelttrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
162 161 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
163 3 43 rrndstprj2 ⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ+ ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝐹 ‘ 𝑘 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) < ( ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
164 129 130 131 146 162 163 syl32anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) < ( ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
165 132 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 𝐷 𝐺 ) ∈ ℂ )
166 140 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℂ )
167 108 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
168 167 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℂ )
169 165 166 168 adddird ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) = ( ( ( 𝐹 𝐷 𝐺 ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) + ( ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
170 165 168 mulcomd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝐹 𝐷 𝐺 ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) = ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
171 124 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℂ )
172 138 rpne0d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
173 171 168 172 divcan1d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) = 𝑟 )
174 170 173 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ( 𝐹 𝐷 𝐺 ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) + ( ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) = ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) )
175 169 174 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( ( ( 𝐹 𝐷 𝐺 ) + ( 𝑟 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) = ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) )
176 164 175 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) < ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) )
177 120 125 176 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ ( 𝐼 ≠ ∅ ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) )
178 177 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 ≠ ∅ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) )
179 178 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 ≠ ∅ ) → ∀ 𝑟 ∈ ℝ+ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) )
180 alrple ⊢ ( ( ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∈ ℝ ∧ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ∈ ℝ ) → ( ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ↔ ∀ 𝑟 ∈ ℝ+ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) ) )
181 82 121 180 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ↔ ∀ 𝑟 ∈ ℝ+ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) ) )
182 181 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 ≠ ∅ ) → ( ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ↔ ∀ 𝑟 ∈ ℝ+ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) + 𝑟 ) ) )
183 179 182 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) ∧ 𝐼 ≠ ∅ ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
184 119 183 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) )
185 87 184 jca ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( ( 𝐹 𝐷 𝐺 ) ≤ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ∧ ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ) )