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	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝐷 = ( 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	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → 𝑋 = ( 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	imbitrrid	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ) → ( 𝐼 = ∅ → 𝐹 = 𝐺 ) )
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 ‘ 𝐼 ) 𝐺 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐹 𝐷 𝐺 ) ) ) )