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 e. ( RR ^m I ) | h finSupp 0 }
rrxmval.d 
|- D = ( dist ` ( RR^ ` I ) )
rrxdstprj1.1 
|- M = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion rrxdstprj1 
|- ( ( ( I e. V /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) M ( G ` A ) ) <_ ( F D G ) )

Proof

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