Metamath Proof Explorer

Theorem prdsxmetlem

Description: The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsdsf.y 
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsdsf.b 
|- B = ( Base ` Y )
prdsdsf.v 
|- V = ( Base ` R )
prdsdsf.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
prdsdsf.d 
|- D = ( dist ` Y )
prdsdsf.s 
|- ( ph -> S e. W )
prdsdsf.i 
|- ( ph -> I e. X )
prdsdsf.r 
|- ( ( ph /\ x e. I ) -> R e. Z )
prdsdsf.m 
|- ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
Assertion prdsxmetlem 
|- ( ph -> D e. ( *Met ` B ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y 
 |-  Y = ( S Xs_ ( x e. I |-> R ) )
2 prdsdsf.b 
 |-  B = ( Base ` Y )
3 prdsdsf.v 
 |-  V = ( Base ` R )
4 prdsdsf.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
5 prdsdsf.d 
 |-  D = ( dist ` Y )
6 prdsdsf.s 
 |-  ( ph -> S e. W )
7 prdsdsf.i 
 |-  ( ph -> I e. X )
8 prdsdsf.r 
 |-  ( ( ph /\ x e. I ) -> R e. Z )
9 prdsdsf.m 
 |-  ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) )
10 2 fvexi 
 |-  B e. _V
11 10 a1i 
 |-  ( ph -> B e. _V )
12 1 2 3 4 5 6 7 8 9 prdsdsf 
 |-  ( ph -> D : ( B X. B ) --> ( 0 [,] +oo ) )
13 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
14 fss 
 |-  ( ( D : ( B X. B ) --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> D : ( B X. B ) --> RR* )
15 12 13 14 sylancl 
 |-  ( ph -> D : ( B X. B ) --> RR* )
16 12 fovrnda 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f D g ) e. ( 0 [,] +oo ) )
17 elxrge0 
 |-  ( ( f D g ) e. ( 0 [,] +oo ) <-> ( ( f D g ) e. RR* /\ 0 <_ ( f D g ) ) )
18 17 simprbi 
 |-  ( ( f D g ) e. ( 0 [,] +oo ) -> 0 <_ ( f D g ) )
19 16 18 syl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> 0 <_ ( f D g ) )
20 6 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> S e. W )
21 7 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> I e. X )
22 8 ralrimiva 
 |-  ( ph -> A. x e. I R e. Z )
23 22 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I R e. Z )
24 simprl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> f e. B )
25 simprr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> g e. B )
26 1 2 20 21 23 24 25 3 4 5 prdsdsval3 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f D g ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
27 26 breq1d 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( ( f D g ) <_ 0 <-> sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) <_ 0 ) )
28 9 adantlr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> E e. ( *Met ` V ) )
29 1 2 20 21 23 3 24 prdsbascl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I ( f ` x ) e. V )
30 29 r19.21bi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( f ` x ) e. V )
31 1 2 20 21 23 3 25 prdsbascl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> A. x e. I ( g ` x ) e. V )
32 31 r19.21bi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( g ` x ) e. V )
33 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ ( f ` x ) e. V /\ ( g ` x ) e. V ) -> ( ( f ` x ) E ( g ` x ) ) e. RR* )
34 28 30 32 33 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( f ` x ) E ( g ` x ) ) e. RR* )
35 34 fmpttd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) : I --> RR* )
36 35 frnd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) C_ RR* )
37 0xr 
 |-  0 e. RR*
38 37 a1i 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> 0 e. RR* )
39 38 snssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> { 0 } C_ RR* )
40 36 39 unssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* )
41 supxrleub 
 |-  ( ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* /\ 0 e. RR* ) -> ( sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) <_ 0 <-> A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ 0 ) )
42 40 37 41 sylancl 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) <_ 0 <-> A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ 0 ) )
43 0le0 
 |-  0 <_ 0
44 c0ex 
 |-  0 e. _V
45 breq1 
 |-  ( z = 0 -> ( z <_ 0 <-> 0 <_ 0 ) )
46 44 45 ralsn 
 |-  ( A. z e. { 0 } z <_ 0 <-> 0 <_ 0 )
47 43 46 mpbir 
 |-  A. z e. { 0 } z <_ 0
48 ralunb 
 |-  ( A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ 0 <-> ( A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ 0 /\ A. z e. { 0 } z <_ 0 ) )
49 47 48 mpbiran2 
 |-  ( A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ 0 <-> A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ 0 )
50 ovex 
 |-  ( ( f ` x ) E ( g ` x ) ) e. _V
51 50 rgenw 
 |-  A. x e. I ( ( f ` x ) E ( g ` x ) ) e. _V
52 eqid 
 |-  ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) )
53 breq1 
 |-  ( z = ( ( f ` x ) E ( g ` x ) ) -> ( z <_ 0 <-> ( ( f ` x ) E ( g ` x ) ) <_ 0 ) )
54 52 53 ralrnmptw 
 |-  ( A. x e. I ( ( f ` x ) E ( g ` x ) ) e. _V -> ( A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ 0 <-> A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ 0 ) )
55 51 54 ax-mp 
 |-  ( A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ 0 <-> A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ 0 )
56 49 55 bitri 
 |-  ( A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ 0 <-> A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ 0 )
57 xmetge0 
 |-  ( ( E e. ( *Met ` V ) /\ ( f ` x ) e. V /\ ( g ` x ) e. V ) -> 0 <_ ( ( f ` x ) E ( g ` x ) ) )
58 28 30 32 57 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> 0 <_ ( ( f ` x ) E ( g ` x ) ) )
59 58 biantrud 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( ( f ` x ) E ( g ` x ) ) <_ 0 <-> ( ( ( f ` x ) E ( g ` x ) ) <_ 0 /\ 0 <_ ( ( f ` x ) E ( g ` x ) ) ) ) )
60 xrletri3 
 |-  ( ( ( ( f ` x ) E ( g ` x ) ) e. RR* /\ 0 e. RR* ) -> ( ( ( f ` x ) E ( g ` x ) ) = 0 <-> ( ( ( f ` x ) E ( g ` x ) ) <_ 0 /\ 0 <_ ( ( f ` x ) E ( g ` x ) ) ) ) )
61 34 37 60 sylancl 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( ( f ` x ) E ( g ` x ) ) = 0 <-> ( ( ( f ` x ) E ( g ` x ) ) <_ 0 /\ 0 <_ ( ( f ` x ) E ( g ` x ) ) ) ) )
62 xmeteq0 
 |-  ( ( E e. ( *Met ` V ) /\ ( f ` x ) e. V /\ ( g ` x ) e. V ) -> ( ( ( f ` x ) E ( g ` x ) ) = 0 <-> ( f ` x ) = ( g ` x ) ) )
63 28 30 32 62 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( ( f ` x ) E ( g ` x ) ) = 0 <-> ( f ` x ) = ( g ` x ) ) )
64 59 61 63 3bitr2d 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B ) ) /\ x e. I ) -> ( ( ( f ` x ) E ( g ` x ) ) <_ 0 <-> ( f ` x ) = ( g ` x ) ) )
65 64 ralbidva 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ 0 <-> A. x e. I ( f ` x ) = ( g ` x ) ) )
66 eqid 
 |-  ( x e. I |-> R ) = ( x e. I |-> R )
67 66 fnmpt 
 |-  ( A. x e. I R e. Z -> ( x e. I |-> R ) Fn I )
68 22 67 syl 
 |-  ( ph -> ( x e. I |-> R ) Fn I )
69 68 adantr 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( x e. I |-> R ) Fn I )
70 1 2 20 21 69 24 prdsbasfn 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> f Fn I )
71 1 2 20 21 69 25 prdsbasfn 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> g Fn I )
72 eqfnfv 
 |-  ( ( f Fn I /\ g Fn I ) -> ( f = g <-> A. x e. I ( f ` x ) = ( g ` x ) ) )
73 70 71 72 syl2anc 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( f = g <-> A. x e. I ( f ` x ) = ( g ` x ) ) )
74 65 73 bitr4d 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ 0 <-> f = g ) )
75 56 74 syl5bb 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ 0 <-> f = g ) )
76 27 42 75 3bitrd 
 |-  ( ( ph /\ ( f e. B /\ g e. B ) ) -> ( ( f D g ) <_ 0 <-> f = g ) )
77 26 3adantr3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) ) -> ( f D g ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
78 77 3adant3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( f D g ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
79 9 3ad2antl1 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> E e. ( *Met ` V ) )
80 29 3adantr3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) ) -> A. x e. I ( f ` x ) e. V )
81 80 3adant3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. x e. I ( f ` x ) e. V )
82 81 r19.21bi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( f ` x ) e. V )
83 31 3adantr3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) ) -> A. x e. I ( g ` x ) e. V )
84 83 3adant3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. x e. I ( g ` x ) e. V )
85 84 r19.21bi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( g ` x ) e. V )
86 79 82 85 33 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( f ` x ) E ( g ` x ) ) e. RR* )
87 6 3ad2ant1 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> S e. W )
88 7 3ad2ant1 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> I e. X )
89 22 3ad2ant1 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. x e. I R e. Z )
90 simp23 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> h e. B )
91 1 2 87 88 89 3 90 prdsbascl 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. x e. I ( h ` x ) e. V )
92 91 r19.21bi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( h ` x ) e. V )
93 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ ( h ` x ) e. V /\ ( f ` x ) e. V ) -> ( ( h ` x ) E ( f ` x ) ) e. RR* )
94 79 92 82 93 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) e. RR* )
95 simp3l 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( h D f ) e. RR )
96 95 adantr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( h D f ) e. RR )
97 xmetge0 
 |-  ( ( E e. ( *Met ` V ) /\ ( h ` x ) e. V /\ ( f ` x ) e. V ) -> 0 <_ ( ( h ` x ) E ( f ` x ) ) )
98 79 92 82 97 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> 0 <_ ( ( h ` x ) E ( f ` x ) ) )
99 94 fmpttd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) : I --> RR* )
100 99 frnd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) C_ RR* )
101 37 a1i 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> 0 e. RR* )
102 101 snssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> { 0 } C_ RR* )
103 100 102 unssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) C_ RR* )
104 ssun1 
 |-  ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) C_ ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } )
105 ovex 
 |-  ( ( h ` x ) E ( f ` x ) ) e. _V
106 105 elabrex 
 |-  ( x e. I -> ( ( h ` x ) E ( f ` x ) ) e. { z | E. x e. I z = ( ( h ` x ) E ( f ` x ) ) } )
107 106 adantl 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) e. { z | E. x e. I z = ( ( h ` x ) E ( f ` x ) ) } )
108 eqid 
 |-  ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) = ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) )
109 108 rnmpt 
 |-  ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) = { z | E. x e. I z = ( ( h ` x ) E ( f ` x ) ) }
110 107 109 eleqtrrdi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) e. ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) )
111 104 110 sselid 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) e. ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) )
112 supxrub 
 |-  ( ( ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) C_ RR* /\ ( ( h ` x ) E ( f ` x ) ) e. ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) ) -> ( ( h ` x ) E ( f ` x ) ) <_ sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
113 103 111 112 syl2an2r 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) <_ sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
114 simp21 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> f e. B )
115 1 2 87 88 89 90 114 3 4 5 prdsdsval3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( h D f ) = sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
116 115 adantr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( h D f ) = sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( f ` x ) ) ) u. { 0 } ) , RR* , < ) )
117 113 116 breqtrrd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) <_ ( h D f ) )
118 xrrege0 
 |-  ( ( ( ( ( h ` x ) E ( f ` x ) ) e. RR* /\ ( h D f ) e. RR ) /\ ( 0 <_ ( ( h ` x ) E ( f ` x ) ) /\ ( ( h ` x ) E ( f ` x ) ) <_ ( h D f ) ) ) -> ( ( h ` x ) E ( f ` x ) ) e. RR )
119 94 96 98 117 118 syl22anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( f ` x ) ) e. RR )
120 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ ( h ` x ) e. V /\ ( g ` x ) e. V ) -> ( ( h ` x ) E ( g ` x ) ) e. RR* )
121 79 92 85 120 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) e. RR* )
122 simp3r 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( h D g ) e. RR )
123 122 adantr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( h D g ) e. RR )
124 xmetge0 
 |-  ( ( E e. ( *Met ` V ) /\ ( h ` x ) e. V /\ ( g ` x ) e. V ) -> 0 <_ ( ( h ` x ) E ( g ` x ) ) )
125 79 92 85 124 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> 0 <_ ( ( h ` x ) E ( g ` x ) ) )
126 121 fmpttd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) : I --> RR* )
127 126 frnd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) C_ RR* )
128 127 102 unssd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* )
129 ssun1 
 |-  ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) C_ ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } )
130 ovex 
 |-  ( ( h ` x ) E ( g ` x ) ) e. _V
131 130 elabrex 
 |-  ( x e. I -> ( ( h ` x ) E ( g ` x ) ) e. { z | E. x e. I z = ( ( h ` x ) E ( g ` x ) ) } )
132 131 adantl 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) e. { z | E. x e. I z = ( ( h ` x ) E ( g ` x ) ) } )
133 eqid 
 |-  ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) = ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) )
134 133 rnmpt 
 |-  ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) = { z | E. x e. I z = ( ( h ` x ) E ( g ` x ) ) }
135 132 134 eleqtrrdi 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) e. ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) )
136 129 135 sselid 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) e. ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) )
137 supxrub 
 |-  ( ( ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* /\ ( ( h ` x ) E ( g ` x ) ) e. ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) ) -> ( ( h ` x ) E ( g ` x ) ) <_ sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
138 128 136 137 syl2an2r 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) <_ sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
139 simp22 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> g e. B )
140 1 2 87 88 89 90 139 3 4 5 prdsdsval3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( h D g ) = sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
141 140 adantr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( h D g ) = sup ( ( ran ( x e. I |-> ( ( h ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
142 138 141 breqtrrd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) <_ ( h D g ) )
143 xrrege0 
 |-  ( ( ( ( ( h ` x ) E ( g ` x ) ) e. RR* /\ ( h D g ) e. RR ) /\ ( 0 <_ ( ( h ` x ) E ( g ` x ) ) /\ ( ( h ` x ) E ( g ` x ) ) <_ ( h D g ) ) ) -> ( ( h ` x ) E ( g ` x ) ) e. RR )
144 121 123 125 142 143 syl22anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h ` x ) E ( g ` x ) ) e. RR )
145 119 144 readdcld 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( ( h ` x ) E ( f ` x ) ) + ( ( h ` x ) E ( g ` x ) ) ) e. RR )
146 79 82 85 57 syl3anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> 0 <_ ( ( f ` x ) E ( g ` x ) ) )
147 xmettri2 
 |-  ( ( E e. ( *Met ` V ) /\ ( ( h ` x ) e. V /\ ( f ` x ) e. V /\ ( g ` x ) e. V ) ) -> ( ( f ` x ) E ( g ` x ) ) <_ ( ( ( h ` x ) E ( f ` x ) ) +e ( ( h ` x ) E ( g ` x ) ) ) )
148 79 92 82 85 147 syl13anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( f ` x ) E ( g ` x ) ) <_ ( ( ( h ` x ) E ( f ` x ) ) +e ( ( h ` x ) E ( g ` x ) ) ) )
149 119 144 rexaddd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( ( h ` x ) E ( f ` x ) ) +e ( ( h ` x ) E ( g ` x ) ) ) = ( ( ( h ` x ) E ( f ` x ) ) + ( ( h ` x ) E ( g ` x ) ) ) )
150 148 149 breqtrd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( f ` x ) E ( g ` x ) ) <_ ( ( ( h ` x ) E ( f ` x ) ) + ( ( h ` x ) E ( g ` x ) ) ) )
151 xrrege0 
 |-  ( ( ( ( ( f ` x ) E ( g ` x ) ) e. RR* /\ ( ( ( h ` x ) E ( f ` x ) ) + ( ( h ` x ) E ( g ` x ) ) ) e. RR ) /\ ( 0 <_ ( ( f ` x ) E ( g ` x ) ) /\ ( ( f ` x ) E ( g ` x ) ) <_ ( ( ( h ` x ) E ( f ` x ) ) + ( ( h ` x ) E ( g ` x ) ) ) ) ) -> ( ( f ` x ) E ( g ` x ) ) e. RR )
152 86 145 146 150 151 syl22anc 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( f ` x ) E ( g ` x ) ) e. RR )
153 readdcl 
 |-  ( ( ( h D f ) e. RR /\ ( h D g ) e. RR ) -> ( ( h D f ) + ( h D g ) ) e. RR )
154 153 3ad2ant3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( ( h D f ) + ( h D g ) ) e. RR )
155 154 adantr 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( h D f ) + ( h D g ) ) e. RR )
156 119 144 96 123 117 142 le2addd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( ( h ` x ) E ( f ` x ) ) + ( ( h ` x ) E ( g ` x ) ) ) <_ ( ( h D f ) + ( h D g ) ) )
157 152 145 155 150 156 letrd 
 |-  ( ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) /\ x e. I ) -> ( ( f ` x ) E ( g ` x ) ) <_ ( ( h D f ) + ( h D g ) ) )
158 157 ralrimiva 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ ( ( h D f ) + ( h D g ) ) )
159 86 ralrimiva 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. x e. I ( ( f ` x ) E ( g ` x ) ) e. RR* )
160 breq1 
 |-  ( z = ( ( f ` x ) E ( g ` x ) ) -> ( z <_ ( ( h D f ) + ( h D g ) ) <-> ( ( f ` x ) E ( g ` x ) ) <_ ( ( h D f ) + ( h D g ) ) ) )
161 52 160 ralrnmptw 
 |-  ( A. x e. I ( ( f ` x ) E ( g ` x ) ) e. RR* -> ( A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ ( ( h D f ) + ( h D g ) ) <-> A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ ( ( h D f ) + ( h D g ) ) ) )
162 159 161 syl 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ ( ( h D f ) + ( h D g ) ) <-> A. x e. I ( ( f ` x ) E ( g ` x ) ) <_ ( ( h D f ) + ( h D g ) ) ) )
163 158 162 mpbird 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ ( ( h D f ) + ( h D g ) ) )
164 12 3ad2ant1 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> D : ( B X. B ) --> ( 0 [,] +oo ) )
165 164 90 114 fovrnd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( h D f ) e. ( 0 [,] +oo ) )
166 elxrge0 
 |-  ( ( h D f ) e. ( 0 [,] +oo ) <-> ( ( h D f ) e. RR* /\ 0 <_ ( h D f ) ) )
167 166 simprbi 
 |-  ( ( h D f ) e. ( 0 [,] +oo ) -> 0 <_ ( h D f ) )
168 165 167 syl 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> 0 <_ ( h D f ) )
169 164 90 139 fovrnd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( h D g ) e. ( 0 [,] +oo ) )
170 elxrge0 
 |-  ( ( h D g ) e. ( 0 [,] +oo ) <-> ( ( h D g ) e. RR* /\ 0 <_ ( h D g ) ) )
171 170 simprbi 
 |-  ( ( h D g ) e. ( 0 [,] +oo ) -> 0 <_ ( h D g ) )
172 169 171 syl 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> 0 <_ ( h D g ) )
173 95 122 168 172 addge0d 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> 0 <_ ( ( h D f ) + ( h D g ) ) )
174 breq1 
 |-  ( z = 0 -> ( z <_ ( ( h D f ) + ( h D g ) ) <-> 0 <_ ( ( h D f ) + ( h D g ) ) ) )
175 44 174 ralsn 
 |-  ( A. z e. { 0 } z <_ ( ( h D f ) + ( h D g ) ) <-> 0 <_ ( ( h D f ) + ( h D g ) ) )
176 173 175 sylibr 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. z e. { 0 } z <_ ( ( h D f ) + ( h D g ) ) )
177 ralunb 
 |-  ( A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ ( ( h D f ) + ( h D g ) ) <-> ( A. z e. ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) z <_ ( ( h D f ) + ( h D g ) ) /\ A. z e. { 0 } z <_ ( ( h D f ) + ( h D g ) ) ) )
178 163 176 177 sylanbrc 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ ( ( h D f ) + ( h D g ) ) )
179 40 3adantr3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) ) -> ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* )
180 179 3adant3 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* )
181 154 rexrd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( ( h D f ) + ( h D g ) ) e. RR* )
182 supxrleub 
 |-  ( ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) C_ RR* /\ ( ( h D f ) + ( h D g ) ) e. RR* ) -> ( sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) <_ ( ( h D f ) + ( h D g ) ) <-> A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ ( ( h D f ) + ( h D g ) ) ) )
183 180 181 182 syl2anc 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) <_ ( ( h D f ) + ( h D g ) ) <-> A. z e. ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) z <_ ( ( h D f ) + ( h D g ) ) ) )
184 178 183 mpbird 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> sup ( ( ran ( x e. I |-> ( ( f ` x ) E ( g ` x ) ) ) u. { 0 } ) , RR* , < ) <_ ( ( h D f ) + ( h D g ) ) )
185 78 184 eqbrtrd 
 |-  ( ( ph /\ ( f e. B /\ g e. B /\ h e. B ) /\ ( ( h D f ) e. RR /\ ( h D g ) e. RR ) ) -> ( f D g ) <_ ( ( h D f ) + ( h D g ) ) )
186 11 15 19 76 185 isxmet2d 
 |-  ( ph -> D e. ( *Met ` B ) )