Metamath Proof Explorer


Theorem 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 I | finSupp 0 h
rrxmval.d D = dist I
rrxdstprj1.1 M = abs 2
Assertion rrxdstprj1 I V A I F X G X F A M G A F D G

Proof

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