rrndstprj2

Description: Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	rrnval.1	$⊢ X = ℝ^{I}$
	rrndstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
Assertion	rrndstprj2	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to F ℝ^{n} (I) G < R \sqrt{\|I\|}$

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	$⊢ X = ℝ^{I}$
2		rrndstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
3		simpl1	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to I \in (Fin ∖ \{\emptyset\})$
4	3	eldifad	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to I \in Fin$
5		simpl2	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to F \in X$
6		simpl3	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to G \in X$
7	1	rrnmval	$⊢ (I \in Fin \land F \in X \land G \in X) \to F ℝ^{n} (I) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
8	4 5 6 7	syl3anc	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to F ℝ^{n} (I) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
9		eldifsni	$⊢ I \in (Fin ∖ \{\emptyset\}) \to I \neq \emptyset$
10	3 9	syl	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to I \neq \emptyset$
11	5 1	eleqtrdi	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to F \in (ℝ^{I})$
12		elmapi	$⊢ F \in (ℝ^{I}) \to F : I ⟶ ℝ$
13	11 12	syl	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to F : I ⟶ ℝ$
14	13	ffvelcdmda	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to F (k) \in ℝ$
15	6 1	eleqtrdi	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to G \in (ℝ^{I})$
16		elmapi	$⊢ G \in (ℝ^{I}) \to G : I ⟶ ℝ$
17	15 16	syl	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to G : I ⟶ ℝ$
18	17	ffvelcdmda	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to G (k) \in ℝ$
19	14 18	resubcld	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to F (k) - G (k) \in ℝ$
20	19	resqcld	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to {(F (k) - G (k))}^{2} \in ℝ$
21		simprl	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R \in ℝ^{+}$
22	21	rpred	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R \in ℝ$
23	22	resqcld	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R^{2} \in ℝ$
24	23	adantr	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to R^{2} \in ℝ$
25		absresq	$⊢ F (k) - G (k) \in ℝ \to {\|F (k) - G (k)\|}^{2} = {(F (k) - G (k))}^{2}$
26	19 25	syl	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to {\|F (k) - G (k)\|}^{2} = {(F (k) - G (k))}^{2}$
27	2	remetdval	$⊢ (F (k) \in ℝ \land G (k) \in ℝ) \to F (k) M G (k) = \|F (k) - G (k)\|$
28	14 18 27	syl2anc	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to F (k) M G (k) = \|F (k) - G (k)\|$
29		simprr	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \forall n \in I F (n) M G (n) < R$
30		fveq2	$⊢ n = k \to F (n) = F (k)$
31		fveq2	$⊢ n = k \to G (n) = G (k)$
32	30 31	oveq12d	$⊢ n = k \to F (n) M G (n) = F (k) M G (k)$
33	32	breq1d	$⊢ n = k \to (F (n) M G (n) < R \leftrightarrow F (k) M G (k) < R)$
34	33	rspccva	$⊢ (\forall n \in I F (n) M G (n) < R \land k \in I) \to F (k) M G (k) < R$
35	29 34	sylan	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to F (k) M G (k) < R$
36	28 35	eqbrtrrd	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to \|F (k) - G (k)\| < R$
37	19	recnd	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to F (k) - G (k) \in ℂ$
38	37	abscld	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to \|F (k) - G (k)\| \in ℝ$
39	22	adantr	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to R \in ℝ$
40	37	absge0d	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to 0 \leq \|F (k) - G (k)\|$
41	21	rpge0d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to 0 \leq R$
42	41	adantr	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to 0 \leq R$
43	38 39 40 42	lt2sqd	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to (\|F (k) - G (k)\| < R \leftrightarrow {\|F (k) - G (k)\|}^{2} < R^{2})$
44	36 43	mpbid	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to {\|F (k) - G (k)\|}^{2} < R^{2}$
45	26 44	eqbrtrrd	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to {(F (k) - G (k))}^{2} < R^{2}$
46	4 10 20 24 45	fsumlt	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sum_{k \in I} {(F (k) - G (k))}^{2} < \sum_{k \in I} R^{2}$
47	4 20	fsumrecl	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sum_{k \in I} {(F (k) - G (k))}^{2} \in ℝ$
48	19	sqge0d	$⊢ (((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \land k \in I) \to 0 \leq {(F (k) - G (k))}^{2}$
49	4 20 48	fsumge0	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to 0 \leq \sum_{k \in I} {(F (k) - G (k))}^{2}$
50		resqrtth	$⊢ (\sum_{k \in I} {(F (k) - G (k))}^{2} \in ℝ \land 0 \leq \sum_{k \in I} {(F (k) - G (k))}^{2}) \to {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2} = \sum_{k \in I} {(F (k) - G (k))}^{2}$
51	47 49 50	syl2anc	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2} = \sum_{k \in I} {(F (k) - G (k))}^{2}$
52		hashnncl	$⊢ I \in Fin \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
53	4 52	syl	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
54	10 53	mpbird	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \|I\| \in ℕ$
55	54	nnrpd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \|I\| \in ℝ^{+}$
56	55	rpred	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \|I\| \in ℝ$
57	55	rpge0d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to 0 \leq \|I\|$
58		resqrtth	$⊢ (\|I\| \in ℝ \land 0 \leq \|I\|) \to {\sqrt{\|I\|}}^{2} = \|I\|$
59	56 57 58	syl2anc	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to {\sqrt{\|I\|}}^{2} = \|I\|$
60	59	oveq2d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R^{2} {\sqrt{\|I\|}}^{2} = R^{2} \|I\|$
61	23	recnd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R^{2} \in ℂ$
62	55	rpcnd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \|I\| \in ℂ$
63	61 62	mulcomd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R^{2} \|I\| = \|I\| R^{2}$
64	60 63	eqtrd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R^{2} {\sqrt{\|I\|}}^{2} = \|I\| R^{2}$
65	21	rpcnd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R \in ℂ$
66	55	rpsqrtcld	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sqrt{\|I\|} \in ℝ^{+}$
67	66	rpcnd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sqrt{\|I\|} \in ℂ$
68	65 67	sqmuld	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to {R \sqrt{\|I\|}}^{2} = R^{2} {\sqrt{\|I\|}}^{2}$
69		fsumconst	$⊢ (I \in Fin \land R^{2} \in ℂ) \to \sum_{k \in I} R^{2} = \|I\| R^{2}$
70	4 61 69	syl2anc	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sum_{k \in I} R^{2} = \|I\| R^{2}$
71	64 68 70	3eqtr4d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to {R \sqrt{\|I\|}}^{2} = \sum_{k \in I} R^{2}$
72	46 51 71	3brtr4d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2} < {R \sqrt{\|I\|}}^{2}$
73	47 49	resqrtcld	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}} \in ℝ$
74	21 66	rpmulcld	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R \sqrt{\|I\|} \in ℝ^{+}$
75	74	rpred	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to R \sqrt{\|I\|} \in ℝ$
76	47 49	sqrtge0d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to 0 \leq \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
77	74	rpge0d	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to 0 \leq R \sqrt{\|I\|}$
78	73 75 76 77	lt2sqd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to (\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}} < R \sqrt{\|I\|} \leftrightarrow {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2} < {R \sqrt{\|I\|}}^{2})$
79	72 78	mpbird	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}} < R \sqrt{\|I\|}$
80	8 79	eqbrtrd	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F \in X \land G \in X) \land (R \in ℝ^{+} \land \forall n \in I F (n) M G (n) < R)) \to F ℝ^{n} (I) G < R \sqrt{\|I\|}$

Metamath Proof Explorer

Theorem rrndstprj2

Proof