rrxdstprj1

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) (Revised by Thierry Arnoux, 7-Jul-2019)

	Ref	Expression
Hypotheses	rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
	rrxmval.d	$⊢ D = dist (I)$
	rrxdstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
Assertion	rrxdstprj1	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to F (A) M G (A) \leq F D G$

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
2		rrxmval.d	$⊢ D = dist (I)$
3		rrxdstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
4		simplll	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to I \in V$
5		simpr	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to A \in ({supp}_{0} (F) \cup {supp}_{0} (G))$
6		simplr	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to (F \in X \land G \in X)$
7		simprl	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F \in X$
8	1 7	rrxfsupp	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F supp 0 \in Fin$
9		simprr	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to G \in X$
10	1 9	rrxfsupp	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to G supp 0 \in Fin$
11		unfi	$⊢ (F supp 0 \in Fin \land G supp 0 \in Fin) \to {supp}_{0} (F) \cup {supp}_{0} (G) \in Fin$
12	8 10 11	syl2anc	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to {supp}_{0} (F) \cup {supp}_{0} (G) \in Fin$
13	1 7	rrxsuppss	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F supp 0 \subseteq I$
14	1 9	rrxsuppss	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to G supp 0 \subseteq I$
15	13 14	unssd	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to {supp}_{0} (F) \cup {supp}_{0} (G) \subseteq I$
16	15	sselda	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to k \in I$
17	1 7	rrxf	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F : I ⟶ ℝ$
18	17	ffvelcdmda	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in I) \to F (k) \in ℝ$
19	1 9	rrxf	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to G : I ⟶ ℝ$
20	19	ffvelcdmda	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in I) \to G (k) \in ℝ$
21	18 20	resubcld	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in I) \to F (k) - G (k) \in ℝ$
22	21	resqcld	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in I) \to {(F (k) - G (k))}^{2} \in ℝ$
23	16 22	syldan	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to {(F (k) - G (k))}^{2} \in ℝ$
24	21	sqge0d	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in I) \to 0 \leq {(F (k) - G (k))}^{2}$
25	16 24	syldan	$⊢ (((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \land k \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to 0 \leq {(F (k) - G (k))}^{2}$
26		fveq2	$⊢ k = A \to F (k) = F (A)$
27		fveq2	$⊢ k = A \to G (k) = G (A)$
28	26 27	oveq12d	$⊢ k = A \to F (k) - G (k) = F (A) - G (A)$
29	28	oveq1d	$⊢ k = A \to {(F (k) - G (k))}^{2} = {(F (A) - G (A))}^{2}$
30		simplr	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to A \in ({supp}_{0} (F) \cup {supp}_{0} (G))$
31	12 23 25 29 30	fsumge1	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to {(F (A) - G (A))}^{2} \leq \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
32	15 30	sseldd	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to A \in I$
33	17 32	ffvelcdmd	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F (A) \in ℝ$
34	19 32	ffvelcdmd	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to G (A) \in ℝ$
35	33 34	resubcld	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F (A) - G (A) \in ℝ$
36		absresq	$⊢ F (A) - G (A) \in ℝ \to {\|F (A) - G (A)\|}^{2} = {(F (A) - G (A))}^{2}$
37	35 36	syl	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to {\|F (A) - G (A)\|}^{2} = {(F (A) - G (A))}^{2}$
38	12 23	fsumrecl	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2} \in ℝ$
39	12 23 25	fsumge0	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to 0 \leq \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
40		resqrtth	$⊢ (\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2} \in ℝ \land 0 \leq \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}) \to {\sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}}^{2} = \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
41	38 39 40	syl2anc	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to {\sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}}^{2} = \sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}$
42	31 37 41	3brtr4d	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to {\|F (A) - G (A)\|}^{2} \leq {\sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}}^{2}$
43	35	recnd	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F (A) - G (A) \in ℂ$
44	43	abscld	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to \|F (A) - G (A)\| \in ℝ$
45	38 39	resqrtcld	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}} \in ℝ$
46	43	absge0d	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to 0 \leq \|F (A) - G (A)\|$
47	38 39	sqrtge0d	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to 0 \leq \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$
48	44 45 46 47	le2sqd	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to (\|F (A) - G (A)\| \leq \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}} \leftrightarrow {\|F (A) - G (A)\|}^{2} \leq {\sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}}^{2})$
49	42 48	mpbird	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to \|F (A) - G (A)\| \leq \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$
50	3	remetdval	$⊢ (F (A) \in ℝ \land G (A) \in ℝ) \to F (A) M G (A) = \|F (A) - G (A)\|$
51	33 34 50	syl2anc	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F (A) M G (A) = \|F (A) - G (A)\|$
52	1 2	rrxmval	$⊢ (I \in V \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$
53	52	3expb	$⊢ (I \in V \land (F \in X \land G \in X)) \to F D G = \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$
54	53	adantlr	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F D G = \sqrt{\sum_{k \in {supp}_{0} (F) \cup {supp}_{0} (G)} {(F (k) - G (k))}^{2}}$
55	49 51 54	3brtr4d	$⊢ ((I \in V \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \land (F \in X \land G \in X)) \to F (A) M G (A) \leq F D G$
56	4 5 6 55	syl21anc	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in ({supp}_{0} (F) \cup {supp}_{0} (G))) \to F (A) M G (A) \leq F D G$
57		simplll	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to I \in V$
58		simplrl	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F \in X$
59		ssun1	$⊢ F supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
60	59	a1i	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to F supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
61	60	sscond	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)) \subseteq I ∖ {supp}_{0} (F)$
62	61	sselda	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to A \in (I ∖ {supp}_{0} (F))$
63		simpr	$⊢ (I \in V \land F \in X) \to F \in X$
64	1 63	rrxf	$⊢ (I \in V \land F \in X) \to F : I ⟶ ℝ$
65		ssidd	$⊢ (I \in V \land F \in X) \to F supp 0 \subseteq F supp 0$
66		simpl	$⊢ (I \in V \land F \in X) \to I \in V$
67		0red	$⊢ (I \in V \land F \in X) \to 0 \in ℝ$
68	64 65 66 67	suppssr	$⊢ ((I \in V \land F \in X) \land A \in (I ∖ {supp}_{0} (F))) \to F (A) = 0$
69	57 58 62 68	syl21anc	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) = 0$
70		0red	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to 0 \in ℝ$
71	69 70	eqeltrd	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) \in ℝ$
72		simplrr	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to G \in X$
73		ssun2	$⊢ G supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
74	73	a1i	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to G supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
75	74	sscond	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)) \subseteq I ∖ {supp}_{0} (G)$
76	75	sselda	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to A \in (I ∖ {supp}_{0} (G))$
77		simpr	$⊢ (I \in V \land G \in X) \to G \in X$
78	1 77	rrxf	$⊢ (I \in V \land G \in X) \to G : I ⟶ ℝ$
79		ssidd	$⊢ (I \in V \land G \in X) \to G supp 0 \subseteq G supp 0$
80		simpl	$⊢ (I \in V \land G \in X) \to I \in V$
81		0red	$⊢ (I \in V \land G \in X) \to 0 \in ℝ$
82	78 79 80 81	suppssr	$⊢ ((I \in V \land G \in X) \land A \in (I ∖ {supp}_{0} (G))) \to G (A) = 0$
83	57 72 76 82	syl21anc	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to G (A) = 0$
84	83 70	eqeltrd	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to G (A) \in ℝ$
85	71 84 50	syl2anc	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) M G (A) = \|F (A) - G (A)\|$
86	69 83	oveq12d	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) - G (A) = 0 - 0$
87		0m0e0	$⊢ 0 - 0 = 0$
88	86 87	eqtrdi	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) - G (A) = 0$
89	88	abs00bd	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to \|F (A) - G (A)\| = 0$
90	85 89	eqtrd	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) M G (A) = 0$
91	1 2	rrxmet	$⊢ I \in V \to D \in Met (X)$
92	91	ad3antrrr	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to D \in Met (X)$
93		metge0	$⊢ (D \in Met (X) \land F \in X \land G \in X) \to 0 \leq F D G$
94	92 58 72 93	syl3anc	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to 0 \leq F D G$
95	90 94	eqbrtrd	$⊢ (((I \in V \land A \in I) \land (F \in X \land G \in X)) \land A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (A) M G (A) \leq F D G$
96		simplr	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to A \in I$
97		simprl	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to F \in X$
98	1 97	rrxsuppss	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to F supp 0 \subseteq I$
99		simprr	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to G \in X$
100	1 99	rrxsuppss	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to G supp 0 \subseteq I$
101	98 100	unssd	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to {supp}_{0} (F) \cup {supp}_{0} (G) \subseteq I$
102		undif	$⊢ {supp}_{0} (F) \cup {supp}_{0} (G) \subseteq I \leftrightarrow ({supp}_{0} (F) \cup {supp}_{0} (G)) \cup (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G))) = I$
103	101 102	sylib	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to ({supp}_{0} (F) \cup {supp}_{0} (G)) \cup (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G))) = I$
104	96 103	eleqtrrd	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to A \in (({supp}_{0} (F) \cup {supp}_{0} (G)) \cup (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G))))$
105		elun	$⊢ A \in (({supp}_{0} (F) \cup {supp}_{0} (G)) \cup (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \leftrightarrow (A \in ({supp}_{0} (F) \cup {supp}_{0} (G)) \lor A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G))))$
106	104 105	sylib	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to (A \in ({supp}_{0} (F) \cup {supp}_{0} (G)) \lor A \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G))))$
107	56 95 106	mpjaodan	$⊢ ((I \in V \land A \in I) \land (F \in X \land G \in X)) \to F (A) M G (A) \leq F D G$

Metamath Proof Explorer

Theorem rrxdstprj1

Proof