Metamath Proof Explorer

Theorem 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 = ( RR ^m I )
rrndstprj1.1 
|- M = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion rrndstprj1 
|- ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) M ( G ` A ) ) <_ ( F ( Rn ` I ) G ) )

Proof

Step Hyp Ref Expression
1 rrnval.1 
 |-  X = ( RR ^m I )
2 rrndstprj1.1 
 |-  M = ( ( abs o. - ) |` ( RR X. RR ) )
3 simpll 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> I e. Fin )
4 simprl 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> F e. X )
5 4 1 eleqtrdi 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> F e. ( RR ^m I ) )
6 elmapi 
 |-  ( F e. ( RR ^m I ) -> F : I --> RR )
7 5 6 syl 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> F : I --> RR )
8 7 ffvelrnda 
 |-  ( ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( F ` k ) e. RR )
9 simprr 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> G e. X )
10 9 1 eleqtrdi 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> G e. ( RR ^m I ) )
11 elmapi 
 |-  ( G e. ( RR ^m I ) -> G : I --> RR )
12 10 11 syl 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> G : I --> RR )
13 12 ffvelrnda 
 |-  ( ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( G ` k ) e. RR )
14 8 13 resubcld 
 |-  ( ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( ( F ` k ) - ( G ` k ) ) e. RR )
15 14 resqcld 
 |-  ( ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. RR )
16 14 sqge0d 
 |-  ( ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> 0 <_ ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
17 fveq2 
 |-  ( k = A -> ( F ` k ) = ( F ` A ) )
18 fveq2 
 |-  ( k = A -> ( G ` k ) = ( G ` A ) )
19 17 18 oveq12d 
 |-  ( k = A -> ( ( F ` k ) - ( G ` k ) ) = ( ( F ` A ) - ( G ` A ) ) )
20 19 oveq1d 
 |-  ( k = A -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = ( ( ( F ` A ) - ( G ` A ) ) ^ 2 ) )
21 simplr 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> A e. I )
22 3 15 16 20 21 fsumge1 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( ( F ` A ) - ( G ` A ) ) ^ 2 ) <_ sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
23 7 21 ffvelrnd 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( F ` A ) e. RR )
24 12 21 ffvelrnd 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( G ` A ) e. RR )
25 23 24 resubcld 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) - ( G ` A ) ) e. RR )
26 absresq 
 |-  ( ( ( F ` A ) - ( G ` A ) ) e. RR -> ( ( abs ` ( ( F ` A ) - ( G ` A ) ) ) ^ 2 ) = ( ( ( F ` A ) - ( G ` A ) ) ^ 2 ) )
27 25 26 syl 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( abs ` ( ( F ` A ) - ( G ` A ) ) ) ^ 2 ) = ( ( ( F ` A ) - ( G ` A ) ) ^ 2 ) )
28 3 15 fsumrecl 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. RR )
29 3 15 16 fsumge0 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> 0 <_ sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
30 resqrtth 
 |-  ( ( sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. RR /\ 0 <_ sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) = sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
31 28 29 30 syl2anc 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) = sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
32 22 27 31 3brtr4d 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( abs ` ( ( F ` A ) - ( G ` A ) ) ) ^ 2 ) <_ ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) )
33 25 recnd 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) - ( G ` A ) ) e. CC )
34 33 abscld 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( abs ` ( ( F ` A ) - ( G ` A ) ) ) e. RR )
35 28 29 resqrtcld 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) e. RR )
36 33 absge0d 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( abs ` ( ( F ` A ) - ( G ` A ) ) ) )
37 28 29 sqrtge0d 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
38 34 35 36 37 le2sqd 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( abs ` ( ( F ` A ) - ( G ` A ) ) ) <_ ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) <-> ( ( abs ` ( ( F ` A ) - ( G ` A ) ) ) ^ 2 ) <_ ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) ) )
39 32 38 mpbird 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( abs ` ( ( F ` A ) - ( G ` A ) ) ) <_ ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
40 2 remetdval 
 |-  ( ( ( F ` A ) e. RR /\ ( G ` A ) e. RR ) -> ( ( F ` A ) M ( G ` A ) ) = ( abs ` ( ( F ` A ) - ( G ` A ) ) ) )
41 23 24 40 syl2anc 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) M ( G ` A ) ) = ( abs ` ( ( F ` A ) - ( G ` A ) ) ) )
42 1 rrnmval 
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( F ( Rn ` I ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
43 42 3expb 
 |-  ( ( I e. Fin /\ ( F e. X /\ G e. X ) ) -> ( F ( Rn ` I ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
44 43 adantlr 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( F ( Rn ` I ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
45 39 41 44 3brtr4d 
 |-  ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) M ( G ` A ) ) <_ ( F ( Rn ` I ) G ) )