Metamath Proof Explorer

Theorem rrnprjdstle

Description: The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses rrnprjdstle.x 
|- ( ph -> X e. Fin )
rrnprjdstle.f 
|- ( ph -> F : X --> RR )
rrnprjdstle.g 
|- ( ph -> G : X --> RR )
rrnprjdstle.i 
|- ( ph -> I e. X )
rrnprjdstle.d 
|- D = ( dist ` ( RR^ ` X ) )
Assertion rrnprjdstle 
|- ( ph -> ( abs ` ( ( F ` I ) - ( G ` I ) ) ) <_ ( F D G ) )

Proof

Step Hyp Ref Expression
1 rrnprjdstle.x 
 |-  ( ph -> X e. Fin )
2 rrnprjdstle.f 
 |-  ( ph -> F : X --> RR )
3 rrnprjdstle.g 
 |-  ( ph -> G : X --> RR )
4 rrnprjdstle.i 
 |-  ( ph -> I e. X )
5 rrnprjdstle.d 
 |-  D = ( dist ` ( RR^ ` X ) )
6 2 4 ffvelrnd 
 |-  ( ph -> ( F ` I ) e. RR )
7 3 4 ffvelrnd 
 |-  ( ph -> ( G ` I ) e. RR )
8 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
9 8 remetdval 
 |-  ( ( ( F ` I ) e. RR /\ ( G ` I ) e. RR ) -> ( ( F ` I ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` I ) ) = ( abs ` ( ( F ` I ) - ( G ` I ) ) ) )
10 6 7 9 syl2anc 
 |-  ( ph -> ( ( F ` I ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` I ) ) = ( abs ` ( ( F ` I ) - ( G ` I ) ) ) )
11 10 eqcomd 
 |-  ( ph -> ( abs ` ( ( F ` I ) - ( G ` I ) ) ) = ( ( F ` I ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` I ) ) )
12 reex 
 |-  RR e. _V
13 12 a1i 
 |-  ( ph -> RR e. _V )
14 13 1 elmapd 
 |-  ( ph -> ( F e. ( RR ^m X ) <-> F : X --> RR ) )
15 2 14 mpbird 
 |-  ( ph -> F e. ( RR ^m X ) )
16 eqid 
 |-  ( RR^ ` X ) = ( RR^ ` X )
17 eqid 
 |-  ( Base ` ( RR^ ` X ) ) = ( Base ` ( RR^ ` X ) )
18 1 16 17 rrxbasefi 
 |-  ( ph -> ( Base ` ( RR^ ` X ) ) = ( RR ^m X ) )
19 16 17 rrxbase 
 |-  ( X e. Fin -> ( Base ` ( RR^ ` X ) ) = { h e. ( RR ^m X ) | h finSupp 0 } )
20 1 19 syl 
 |-  ( ph -> ( Base ` ( RR^ ` X ) ) = { h e. ( RR ^m X ) | h finSupp 0 } )
21 18 20 eqtr3d 
 |-  ( ph -> ( RR ^m X ) = { h e. ( RR ^m X ) | h finSupp 0 } )
22 15 21 eleqtrd 
 |-  ( ph -> F e. { h e. ( RR ^m X ) | h finSupp 0 } )
23 13 1 elmapd 
 |-  ( ph -> ( G e. ( RR ^m X ) <-> G : X --> RR ) )
24 3 23 mpbird 
 |-  ( ph -> G e. ( RR ^m X ) )
25 24 21 eleqtrd 
 |-  ( ph -> G e. { h e. ( RR ^m X ) | h finSupp 0 } )
26 eqid 
 |-  { h e. ( RR ^m X ) | h finSupp 0 } = { h e. ( RR ^m X ) | h finSupp 0 }
27 26 5 8 rrxdstprj1 
 |-  ( ( ( X e. Fin /\ I e. X ) /\ ( F e. { h e. ( RR ^m X ) | h finSupp 0 } /\ G e. { h e. ( RR ^m X ) | h finSupp 0 } ) ) -> ( ( F ` I ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` I ) ) <_ ( F D G ) )
28 1 4 22 25 27 syl22anc 
 |-  ( ph -> ( ( F ` I ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` I ) ) <_ ( F D G ) )
29 11 28 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( F ` I ) - ( G ` I ) ) ) <_ ( F D G ) )