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	$⊢ Y = (ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I$
	rrnequiv.d	$⊢ D = dist (Y)$
	rrnequiv.1	$⊢ X = ℝ^{I}$
	rrnequiv.i	$⊢ φ \to I \in Fin$
Assertion	rrnequiv	$⊢ (φ \land (F \in X \land G \in X)) \to (F D G \leq F ℝ^{n} (I) G \land F ℝ^{n} (I) G \leq \sqrt{\|I\|} (F D G))$

Proof

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

Metamath Proof Explorer

Theorem rrnequiv

Proof