rrndstprj1

Description: The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (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	rrndstprj1	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F (A) M G (A) \leq F ℝ^{n} (I) G$

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	$⊢ X = ℝ^{I}$
2		rrndstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
3		simpll	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to I \in Fin$
4		simprl	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F \in X$
5	4 1	eleqtrdi	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F \in (ℝ^{I})$
6		elmapi	$⊢ F \in (ℝ^{I}) \to F : I ⟶ ℝ$
7	5 6	syl	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F : I ⟶ ℝ$
8	7	ffvelrnda	$⊢ (((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \land k \in I) \to F (k) \in ℝ$
9		simprr	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to G \in X$
10	9 1	eleqtrdi	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to G \in (ℝ^{I})$
11		elmapi	$⊢ G \in (ℝ^{I}) \to G : I ⟶ ℝ$
12	10 11	syl	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to G : I ⟶ ℝ$
13	12	ffvelrnda	$⊢ (((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \land k \in I) \to G (k) \in ℝ$
14	8 13	resubcld	$⊢ (((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \land k \in I) \to F (k) - G (k) \in ℝ$
15	14	resqcld	$⊢ (((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \land k \in I) \to {(F (k) - G (k))}^{2} \in ℝ$
16	14	sqge0d	$⊢ (((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \land k \in I) \to 0 \leq {(F (k) - G (k))}^{2}$
17		fveq2	$⊢ k = A \to F (k) = F (A)$
18		fveq2	$⊢ k = A \to G (k) = G (A)$
19	17 18	oveq12d	$⊢ k = A \to F (k) - G (k) = F (A) - G (A)$
20	19	oveq1d	$⊢ k = A \to {(F (k) - G (k))}^{2} = {(F (A) - G (A))}^{2}$
21		simplr	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to A \in I$
22	3 15 16 20 21	fsumge1	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to {(F (A) - G (A))}^{2} \leq \sum_{k \in I} {(F (k) - G (k))}^{2}$
23	7 21	ffvelrnd	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F (A) \in ℝ$
24	12 21	ffvelrnd	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to G (A) \in ℝ$
25	23 24	resubcld	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F (A) - G (A) \in ℝ$
26		absresq	$⊢ F (A) - G (A) \in ℝ \to {\|F (A) - G (A)\|}^{2} = {(F (A) - G (A))}^{2}$
27	25 26	syl	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to {\|F (A) - G (A)\|}^{2} = {(F (A) - G (A))}^{2}$
28	3 15	fsumrecl	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to \sum_{k \in I} {(F (k) - G (k))}^{2} \in ℝ$
29	3 15 16	fsumge0	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to 0 \leq \sum_{k \in I} {(F (k) - G (k))}^{2}$
30		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}$
31	28 29 30	syl2anc	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2} = \sum_{k \in I} {(F (k) - G (k))}^{2}$
32	22 27 31	3brtr4d	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to {\|F (A) - G (A)\|}^{2} \leq {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2}$
33	25	recnd	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F (A) - G (A) \in ℂ$
34	33	abscld	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to \|F (A) - G (A)\| \in ℝ$
35	28 29	resqrtcld	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}} \in ℝ$
36	33	absge0d	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to 0 \leq \|F (A) - G (A)\|$
37	28 29	sqrtge0d	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to 0 \leq \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
38	34 35 36 37	le2sqd	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to (\|F (A) - G (A)\| \leq \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}} \leftrightarrow {\|F (A) - G (A)\|}^{2} \leq {\sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}}^{2})$
39	32 38	mpbird	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to \|F (A) - G (A)\| \leq \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
40	2	remetdval	$⊢ (F (A) \in ℝ \land G (A) \in ℝ) \to F (A) M G (A) = \|F (A) - G (A)\|$
41	23 24 40	syl2anc	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F (A) M G (A) = \|F (A) - G (A)\|$
42	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}}$
43	42	3expb	$⊢ (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}}$
44	43	adantlr	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F ℝ^{n} (I) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
45	39 41 44	3brtr4d	$⊢ ((I \in Fin \land A \in I) \land (F \in X \land G \in X)) \to F (A) M G (A) \leq F ℝ^{n} (I) G$

Metamath Proof Explorer

Theorem rrndstprj1

Proof