Metamath Proof Explorer

Theorem nrmmetd

Description: Show that a group norm generates a metric. Part of Definition 2.2-1 of Kreyszig p. 58. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nrmmetd.x 
|- X = ( Base ` G )
nrmmetd.m 
|- .- = ( -g ` G )
nrmmetd.z 
|- .0. = ( 0g ` G )
nrmmetd.g 
|- ( ph -> G e. Grp )
nrmmetd.f 
|- ( ph -> F : X --> RR )
nrmmetd.1 
|- ( ( ph /\ x e. X ) -> ( ( F ` x ) = 0 <-> x = .0. ) )
nrmmetd.2 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
Assertion nrmmetd 
|- ( ph -> ( F o. .- ) e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 nrmmetd.x 
 |-  X = ( Base ` G )
2 nrmmetd.m 
 |-  .- = ( -g ` G )
3 nrmmetd.z 
 |-  .0. = ( 0g ` G )
4 nrmmetd.g 
 |-  ( ph -> G e. Grp )
5 nrmmetd.f 
 |-  ( ph -> F : X --> RR )
6 nrmmetd.1 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) = 0 <-> x = .0. ) )
7 nrmmetd.2 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
8 1 2 grpsubf 
 |-  ( G e. Grp -> .- : ( X X. X ) --> X )
9 4 8 syl 
 |-  ( ph -> .- : ( X X. X ) --> X )
10 fco 
 |-  ( ( F : X --> RR /\ .- : ( X X. X ) --> X ) -> ( F o. .- ) : ( X X. X ) --> RR )
11 5 9 10 syl2anc 
 |-  ( ph -> ( F o. .- ) : ( X X. X ) --> RR )
12 opelxpi 
 |-  ( ( a e. X /\ b e. X ) -> <. a , b >. e. ( X X. X ) )
13 fvco3 
 |-  ( ( .- : ( X X. X ) --> X /\ <. a , b >. e. ( X X. X ) ) -> ( ( F o. .- ) ` <. a , b >. ) = ( F ` ( .- ` <. a , b >. ) ) )
14 9 12 13 syl2an 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( F o. .- ) ` <. a , b >. ) = ( F ` ( .- ` <. a , b >. ) ) )
15 df-ov 
 |-  ( a ( F o. .- ) b ) = ( ( F o. .- ) ` <. a , b >. )
16 df-ov 
 |-  ( a .- b ) = ( .- ` <. a , b >. )
17 16 fveq2i 
 |-  ( F ` ( a .- b ) ) = ( F ` ( .- ` <. a , b >. ) )
18 14 15 17 3eqtr4g 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( a ( F o. .- ) b ) = ( F ` ( a .- b ) ) )
19 18 eqeq1d 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( a ( F o. .- ) b ) = 0 <-> ( F ` ( a .- b ) ) = 0 ) )
20 6 ralrimiva 
 |-  ( ph -> A. x e. X ( ( F ` x ) = 0 <-> x = .0. ) )
21 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ a e. X /\ b e. X ) -> ( a .- b ) e. X )
22 21 3expb 
 |-  ( ( G e. Grp /\ ( a e. X /\ b e. X ) ) -> ( a .- b ) e. X )
23 4 22 sylan 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( a .- b ) e. X )
24 fveq2 
 |-  ( x = ( a .- b ) -> ( F ` x ) = ( F ` ( a .- b ) ) )
25 24 eqeq1d 
 |-  ( x = ( a .- b ) -> ( ( F ` x ) = 0 <-> ( F ` ( a .- b ) ) = 0 ) )
26 eqeq1 
 |-  ( x = ( a .- b ) -> ( x = .0. <-> ( a .- b ) = .0. ) )
27 25 26 bibi12d 
 |-  ( x = ( a .- b ) -> ( ( ( F ` x ) = 0 <-> x = .0. ) <-> ( ( F ` ( a .- b ) ) = 0 <-> ( a .- b ) = .0. ) ) )
28 27 rspccva 
 |-  ( ( A. x e. X ( ( F ` x ) = 0 <-> x = .0. ) /\ ( a .- b ) e. X ) -> ( ( F ` ( a .- b ) ) = 0 <-> ( a .- b ) = .0. ) )
29 20 23 28 syl2an2r 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( F ` ( a .- b ) ) = 0 <-> ( a .- b ) = .0. ) )
30 1 3 2 grpsubeq0 
 |-  ( ( G e. Grp /\ a e. X /\ b e. X ) -> ( ( a .- b ) = .0. <-> a = b ) )
31 30 3expb 
 |-  ( ( G e. Grp /\ ( a e. X /\ b e. X ) ) -> ( ( a .- b ) = .0. <-> a = b ) )
32 4 31 sylan 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( a .- b ) = .0. <-> a = b ) )
33 19 29 32 3bitrd 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( a ( F o. .- ) b ) = 0 <-> a = b ) )
34 5 adantr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> F : X --> RR )
35 23 adantrr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( a .- b ) e. X )
36 34 35 ffvelcdmd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( a .- b ) ) e. RR )
37 4 adantr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> G e. Grp )
38 simprll 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> a e. X )
39 simprr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> c e. X )
40 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ a e. X /\ c e. X ) -> ( a .- c ) e. X )
41 37 38 39 40 syl3anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( a .- c ) e. X )
42 34 41 ffvelcdmd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( a .- c ) ) e. RR )
43 simprlr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> b e. X )
44 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ b e. X /\ c e. X ) -> ( b .- c ) e. X )
45 37 43 39 44 syl3anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( b .- c ) e. X )
46 34 45 ffvelcdmd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( b .- c ) ) e. RR )
47 42 46 readdcld 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) e. RR )
48 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ c e. X /\ a e. X ) -> ( c .- a ) e. X )
49 37 39 38 48 syl3anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( c .- a ) e. X )
50 34 49 ffvelcdmd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( c .- a ) ) e. RR )
51 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ c e. X /\ b e. X ) -> ( c .- b ) e. X )
52 37 39 43 51 syl3anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( c .- b ) e. X )
53 34 52 ffvelcdmd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( c .- b ) ) e. RR )
54 50 53 readdcld 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( F ` ( c .- a ) ) + ( F ` ( c .- b ) ) ) e. RR )
55 1 2 grpnnncan2 
 |-  ( ( G e. Grp /\ ( a e. X /\ b e. X /\ c e. X ) ) -> ( ( a .- c ) .- ( b .- c ) ) = ( a .- b ) )
56 37 38 43 39 55 syl13anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( a .- c ) .- ( b .- c ) ) = ( a .- b ) )
57 56 fveq2d 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( ( a .- c ) .- ( b .- c ) ) ) = ( F ` ( a .- b ) ) )
58 7 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. X ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
59 58 adantr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> A. x e. X A. y e. X ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
60 fvoveq1 
 |-  ( x = ( a .- c ) -> ( F ` ( x .- y ) ) = ( F ` ( ( a .- c ) .- y ) ) )
61 fveq2 
 |-  ( x = ( a .- c ) -> ( F ` x ) = ( F ` ( a .- c ) ) )
62 61 oveq1d 
 |-  ( x = ( a .- c ) -> ( ( F ` x ) + ( F ` y ) ) = ( ( F ` ( a .- c ) ) + ( F ` y ) ) )
63 60 62 breq12d 
 |-  ( x = ( a .- c ) -> ( ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) <-> ( F ` ( ( a .- c ) .- y ) ) <_ ( ( F ` ( a .- c ) ) + ( F ` y ) ) ) )
64 oveq2 
 |-  ( y = ( b .- c ) -> ( ( a .- c ) .- y ) = ( ( a .- c ) .- ( b .- c ) ) )
65 64 fveq2d 
 |-  ( y = ( b .- c ) -> ( F ` ( ( a .- c ) .- y ) ) = ( F ` ( ( a .- c ) .- ( b .- c ) ) ) )
66 fveq2 
 |-  ( y = ( b .- c ) -> ( F ` y ) = ( F ` ( b .- c ) ) )
67 66 oveq2d 
 |-  ( y = ( b .- c ) -> ( ( F ` ( a .- c ) ) + ( F ` y ) ) = ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) )
68 65 67 breq12d 
 |-  ( y = ( b .- c ) -> ( ( F ` ( ( a .- c ) .- y ) ) <_ ( ( F ` ( a .- c ) ) + ( F ` y ) ) <-> ( F ` ( ( a .- c ) .- ( b .- c ) ) ) <_ ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) ) )
69 63 68 rspc2va 
 |-  ( ( ( ( a .- c ) e. X /\ ( b .- c ) e. X ) /\ A. x e. X A. y e. X ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) -> ( F ` ( ( a .- c ) .- ( b .- c ) ) ) <_ ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) )
70 41 45 59 69 syl21anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( ( a .- c ) .- ( b .- c ) ) ) <_ ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) )
71 57 70 eqbrtrrd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( a .- b ) ) <_ ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) )
72 eleq1w 
 |-  ( b = c -> ( b e. X <-> c e. X ) )
73 72 anbi2d 
 |-  ( b = c -> ( ( a e. X /\ b e. X ) <-> ( a e. X /\ c e. X ) ) )
74 73 anbi2d 
 |-  ( b = c -> ( ( ph /\ ( a e. X /\ b e. X ) ) <-> ( ph /\ ( a e. X /\ c e. X ) ) ) )
75 oveq2 
 |-  ( b = c -> ( a .- b ) = ( a .- c ) )
76 75 fveq2d 
 |-  ( b = c -> ( F ` ( a .- b ) ) = ( F ` ( a .- c ) ) )
77 fvoveq1 
 |-  ( b = c -> ( F ` ( b .- a ) ) = ( F ` ( c .- a ) ) )
78 76 77 breq12d 
 |-  ( b = c -> ( ( F ` ( a .- b ) ) <_ ( F ` ( b .- a ) ) <-> ( F ` ( a .- c ) ) <_ ( F ` ( c .- a ) ) ) )
79 74 78 imbi12d 
 |-  ( b = c -> ( ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` ( a .- b ) ) <_ ( F ` ( b .- a ) ) ) <-> ( ( ph /\ ( a e. X /\ c e. X ) ) -> ( F ` ( a .- c ) ) <_ ( F ` ( c .- a ) ) ) ) )
80 4 adantr 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> G e. Grp )
81 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. X )
82 80 81 syl 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> .0. e. X )
83 simprr 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> b e. X )
84 simprl 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> a e. X )
85 1 2 grpsubcl 
 |-  ( ( G e. Grp /\ b e. X /\ a e. X ) -> ( b .- a ) e. X )
86 80 83 84 85 syl3anc 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( b .- a ) e. X )
87 58 adantr 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> A. x e. X A. y e. X ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )
88 fvoveq1 
 |-  ( x = .0. -> ( F ` ( x .- y ) ) = ( F ` ( .0. .- y ) ) )
89 fveq2 
 |-  ( x = .0. -> ( F ` x ) = ( F ` .0. ) )
90 89 oveq1d 
 |-  ( x = .0. -> ( ( F ` x ) + ( F ` y ) ) = ( ( F ` .0. ) + ( F ` y ) ) )
91 88 90 breq12d 
 |-  ( x = .0. -> ( ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) <-> ( F ` ( .0. .- y ) ) <_ ( ( F ` .0. ) + ( F ` y ) ) ) )
92 oveq2 
 |-  ( y = ( b .- a ) -> ( .0. .- y ) = ( .0. .- ( b .- a ) ) )
93 92 fveq2d 
 |-  ( y = ( b .- a ) -> ( F ` ( .0. .- y ) ) = ( F ` ( .0. .- ( b .- a ) ) ) )
94 fveq2 
 |-  ( y = ( b .- a ) -> ( F ` y ) = ( F ` ( b .- a ) ) )
95 94 oveq2d 
 |-  ( y = ( b .- a ) -> ( ( F ` .0. ) + ( F ` y ) ) = ( ( F ` .0. ) + ( F ` ( b .- a ) ) ) )
96 93 95 breq12d 
 |-  ( y = ( b .- a ) -> ( ( F ` ( .0. .- y ) ) <_ ( ( F ` .0. ) + ( F ` y ) ) <-> ( F ` ( .0. .- ( b .- a ) ) ) <_ ( ( F ` .0. ) + ( F ` ( b .- a ) ) ) ) )
97 91 96 rspc2va 
 |-  ( ( ( .0. e. X /\ ( b .- a ) e. X ) /\ A. x e. X A. y e. X ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) -> ( F ` ( .0. .- ( b .- a ) ) ) <_ ( ( F ` .0. ) + ( F ` ( b .- a ) ) ) )
98 82 86 87 97 syl21anc 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` ( .0. .- ( b .- a ) ) ) <_ ( ( F ` .0. ) + ( F ` ( b .- a ) ) ) )
99 eqid 
 |-  ( invg ` G ) = ( invg ` G )
100 1 2 99 3 grpinvval2 
 |-  ( ( G e. Grp /\ ( b .- a ) e. X ) -> ( ( invg ` G ) ` ( b .- a ) ) = ( .0. .- ( b .- a ) ) )
101 4 86 100 syl2an2r 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( invg ` G ) ` ( b .- a ) ) = ( .0. .- ( b .- a ) ) )
102 1 2 99 grpinvsub 
 |-  ( ( G e. Grp /\ b e. X /\ a e. X ) -> ( ( invg ` G ) ` ( b .- a ) ) = ( a .- b ) )
103 80 83 84 102 syl3anc 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( invg ` G ) ` ( b .- a ) ) = ( a .- b ) )
104 101 103 eqtr3d 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( .0. .- ( b .- a ) ) = ( a .- b ) )
105 104 fveq2d 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` ( .0. .- ( b .- a ) ) ) = ( F ` ( a .- b ) ) )
106 4 81 syl 
 |-  ( ph -> .0. e. X )
107 pm5.501 
 |-  ( x = .0. -> ( ( F ` x ) = 0 <-> ( x = .0. <-> ( F ` x ) = 0 ) ) )
108 bicom 
 |-  ( ( x = .0. <-> ( F ` x ) = 0 ) <-> ( ( F ` x ) = 0 <-> x = .0. ) )
109 107 108 bitrdi 
 |-  ( x = .0. -> ( ( F ` x ) = 0 <-> ( ( F ` x ) = 0 <-> x = .0. ) ) )
110 89 eqeq1d 
 |-  ( x = .0. -> ( ( F ` x ) = 0 <-> ( F ` .0. ) = 0 ) )
111 109 110 bitr3d 
 |-  ( x = .0. -> ( ( ( F ` x ) = 0 <-> x = .0. ) <-> ( F ` .0. ) = 0 ) )
112 111 rspccva 
 |-  ( ( A. x e. X ( ( F ` x ) = 0 <-> x = .0. ) /\ .0. e. X ) -> ( F ` .0. ) = 0 )
113 20 106 112 syl2anc 
 |-  ( ph -> ( F ` .0. ) = 0 )
114 113 adantr 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` .0. ) = 0 )
115 114 oveq1d 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( F ` .0. ) + ( F ` ( b .- a ) ) ) = ( 0 + ( F ` ( b .- a ) ) ) )
116 5 adantr 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> F : X --> RR )
117 116 86 ffvelcdmd 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` ( b .- a ) ) e. RR )
118 117 recnd 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` ( b .- a ) ) e. CC )
119 118 addlidd 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( 0 + ( F ` ( b .- a ) ) ) = ( F ` ( b .- a ) ) )
120 115 119 eqtrd 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( F ` .0. ) + ( F ` ( b .- a ) ) ) = ( F ` ( b .- a ) ) )
121 98 105 120 3brtr3d 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( F ` ( a .- b ) ) <_ ( F ` ( b .- a ) ) )
122 79 121 chvarvv 
 |-  ( ( ph /\ ( a e. X /\ c e. X ) ) -> ( F ` ( a .- c ) ) <_ ( F ` ( c .- a ) ) )
123 122 adantrlr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( a .- c ) ) <_ ( F ` ( c .- a ) ) )
124 eleq1w 
 |-  ( a = b -> ( a e. X <-> b e. X ) )
125 124 anbi1d 
 |-  ( a = b -> ( ( a e. X /\ c e. X ) <-> ( b e. X /\ c e. X ) ) )
126 125 anbi2d 
 |-  ( a = b -> ( ( ph /\ ( a e. X /\ c e. X ) ) <-> ( ph /\ ( b e. X /\ c e. X ) ) ) )
127 fvoveq1 
 |-  ( a = b -> ( F ` ( a .- c ) ) = ( F ` ( b .- c ) ) )
128 oveq2 
 |-  ( a = b -> ( c .- a ) = ( c .- b ) )
129 128 fveq2d 
 |-  ( a = b -> ( F ` ( c .- a ) ) = ( F ` ( c .- b ) ) )
130 127 129 breq12d 
 |-  ( a = b -> ( ( F ` ( a .- c ) ) <_ ( F ` ( c .- a ) ) <-> ( F ` ( b .- c ) ) <_ ( F ` ( c .- b ) ) ) )
131 126 130 imbi12d 
 |-  ( a = b -> ( ( ( ph /\ ( a e. X /\ c e. X ) ) -> ( F ` ( a .- c ) ) <_ ( F ` ( c .- a ) ) ) <-> ( ( ph /\ ( b e. X /\ c e. X ) ) -> ( F ` ( b .- c ) ) <_ ( F ` ( c .- b ) ) ) ) )
132 131 122 chvarvv 
 |-  ( ( ph /\ ( b e. X /\ c e. X ) ) -> ( F ` ( b .- c ) ) <_ ( F ` ( c .- b ) ) )
133 132 adantrll 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( b .- c ) ) <_ ( F ` ( c .- b ) ) )
134 42 46 50 53 123 133 le2addd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( F ` ( a .- c ) ) + ( F ` ( b .- c ) ) ) <_ ( ( F ` ( c .- a ) ) + ( F ` ( c .- b ) ) ) )
135 36 47 54 71 134 letrd 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( F ` ( a .- b ) ) <_ ( ( F ` ( c .- a ) ) + ( F ` ( c .- b ) ) ) )
136 18 adantrr 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( a ( F o. .- ) b ) = ( F ` ( a .- b ) ) )
137 opelxpi 
 |-  ( ( c e. X /\ a e. X ) -> <. c , a >. e. ( X X. X ) )
138 39 38 137 syl2anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> <. c , a >. e. ( X X. X ) )
139 fvco3 
 |-  ( ( .- : ( X X. X ) --> X /\ <. c , a >. e. ( X X. X ) ) -> ( ( F o. .- ) ` <. c , a >. ) = ( F ` ( .- ` <. c , a >. ) ) )
140 9 138 139 syl2an2r 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( F o. .- ) ` <. c , a >. ) = ( F ` ( .- ` <. c , a >. ) ) )
141 df-ov 
 |-  ( c ( F o. .- ) a ) = ( ( F o. .- ) ` <. c , a >. )
142 df-ov 
 |-  ( c .- a ) = ( .- ` <. c , a >. )
143 142 fveq2i 
 |-  ( F ` ( c .- a ) ) = ( F ` ( .- ` <. c , a >. ) )
144 140 141 143 3eqtr4g 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( c ( F o. .- ) a ) = ( F ` ( c .- a ) ) )
145 opelxpi 
 |-  ( ( c e. X /\ b e. X ) -> <. c , b >. e. ( X X. X ) )
146 39 43 145 syl2anc 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> <. c , b >. e. ( X X. X ) )
147 fvco3 
 |-  ( ( .- : ( X X. X ) --> X /\ <. c , b >. e. ( X X. X ) ) -> ( ( F o. .- ) ` <. c , b >. ) = ( F ` ( .- ` <. c , b >. ) ) )
148 9 146 147 syl2an2r 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( F o. .- ) ` <. c , b >. ) = ( F ` ( .- ` <. c , b >. ) ) )
149 df-ov 
 |-  ( c ( F o. .- ) b ) = ( ( F o. .- ) ` <. c , b >. )
150 df-ov 
 |-  ( c .- b ) = ( .- ` <. c , b >. )
151 150 fveq2i 
 |-  ( F ` ( c .- b ) ) = ( F ` ( .- ` <. c , b >. ) )
152 148 149 151 3eqtr4g 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( c ( F o. .- ) b ) = ( F ` ( c .- b ) ) )
153 144 152 oveq12d 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) = ( ( F ` ( c .- a ) ) + ( F ` ( c .- b ) ) ) )
154 135 136 153 3brtr4d 
 |-  ( ( ph /\ ( ( a e. X /\ b e. X ) /\ c e. X ) ) -> ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) )
155 154 expr 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( c e. X -> ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) ) )
156 155 ralrimiv 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> A. c e. X ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) )
157 33 156 jca 
 |-  ( ( ph /\ ( a e. X /\ b e. X ) ) -> ( ( ( a ( F o. .- ) b ) = 0 <-> a = b ) /\ A. c e. X ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) ) )
158 157 ralrimivva 
 |-  ( ph -> A. a e. X A. b e. X ( ( ( a ( F o. .- ) b ) = 0 <-> a = b ) /\ A. c e. X ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) ) )
159 1 fvexi 
 |-  X e. _V
160 ismet 
 |-  ( X e. _V -> ( ( F o. .- ) e. ( Met ` X ) <-> ( ( F o. .- ) : ( X X. X ) --> RR /\ A. a e. X A. b e. X ( ( ( a ( F o. .- ) b ) = 0 <-> a = b ) /\ A. c e. X ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) ) ) ) )
161 159 160 ax-mp 
 |-  ( ( F o. .- ) e. ( Met ` X ) <-> ( ( F o. .- ) : ( X X. X ) --> RR /\ A. a e. X A. b e. X ( ( ( a ( F o. .- ) b ) = 0 <-> a = b ) /\ A. c e. X ( a ( F o. .- ) b ) <_ ( ( c ( F o. .- ) a ) + ( c ( F o. .- ) b ) ) ) ) )
162 11 158 161 sylanbrc 
 |-  ( ph -> ( F o. .- ) e. ( Met ` X ) )