Metamath Proof Explorer

Theorem abvcxp

Description: Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvcxp.a 
|- A = ( AbsVal ` R )
abvcxp.b 
|- B = ( Base ` R )
abvcxp.f 
|- G = ( x e. B |-> ( ( F ` x ) ^c S ) )
Assertion abvcxp 
|- ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> G e. A )

Proof

Step Hyp Ref Expression
1 abvcxp.a 
 |-  A = ( AbsVal ` R )
2 abvcxp.b 
 |-  B = ( Base ` R )
3 abvcxp.f 
 |-  G = ( x e. B |-> ( ( F ` x ) ^c S ) )
4 1 a1i 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> A = ( AbsVal ` R ) )
5 2 a1i 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> B = ( Base ` R ) )
6 eqidd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( +g ` R ) = ( +g ` R ) )
7 eqidd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( .r ` R ) = ( .r ` R ) )
8 eqidd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( 0g ` R ) = ( 0g ` R ) )
9 1 abvrcl 
 |-  ( F e. A -> R e. Ring )
10 9 adantr 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> R e. Ring )
11 1 2 abvcl 
 |-  ( ( F e. A /\ x e. B ) -> ( F ` x ) e. RR )
12 11 adantlr 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ x e. B ) -> ( F ` x ) e. RR )
13 1 2 abvge0 
 |-  ( ( F e. A /\ x e. B ) -> 0 <_ ( F ` x ) )
14 13 adantlr 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ x e. B ) -> 0 <_ ( F ` x ) )
15 0xr 
 |-  0 e. RR*
16 1re 
 |-  1 e. RR
17 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( S e. ( 0 (,] 1 ) <-> ( S e. RR /\ 0 < S /\ S <_ 1 ) ) )
18 15 16 17 mp2an 
 |-  ( S e. ( 0 (,] 1 ) <-> ( S e. RR /\ 0 < S /\ S <_ 1 ) )
19 18 bilani 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( S e. RR /\ 0 < S /\ S <_ 1 ) )
20 19 simp1d 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> S e. RR )
21 20 adantr 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ x e. B ) -> S e. RR )
22 12 14 21 recxpcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ x e. B ) -> ( ( F ` x ) ^c S ) e. RR )
23 22 3 fmptd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> G : B --> RR )
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 2 24 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. B )
26 10 25 syl 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( 0g ` R ) e. B )
27 fveq2 
 |-  ( x = ( 0g ` R ) -> ( F ` x ) = ( F ` ( 0g ` R ) ) )
28 27 oveq1d 
 |-  ( x = ( 0g ` R ) -> ( ( F ` x ) ^c S ) = ( ( F ` ( 0g ` R ) ) ^c S ) )
29 ovex 
 |-  ( ( F ` ( 0g ` R ) ) ^c S ) e. _V
30 28 3 29 fvmpt 
 |-  ( ( 0g ` R ) e. B -> ( G ` ( 0g ` R ) ) = ( ( F ` ( 0g ` R ) ) ^c S ) )
31 26 30 syl 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( G ` ( 0g ` R ) ) = ( ( F ` ( 0g ` R ) ) ^c S ) )
32 1 24 abv0 
 |-  ( F e. A -> ( F ` ( 0g ` R ) ) = 0 )
33 32 adantr 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( F ` ( 0g ` R ) ) = 0 )
34 33 oveq1d 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( ( F ` ( 0g ` R ) ) ^c S ) = ( 0 ^c S ) )
35 20 recnd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> S e. CC )
36 19 simp2d 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> 0 < S )
37 36 gt0ne0d 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> S =/= 0 )
38 35 37 0cxpd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( 0 ^c S ) = 0 )
39 34 38 eqtrd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( ( F ` ( 0g ` R ) ) ^c S ) = 0 )
40 31 39 eqtrd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> ( G ` ( 0g ` R ) ) = 0 )
41 simp1l 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> F e. A )
42 simp2 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> y e. B )
43 1 2 abvcl 
 |-  ( ( F e. A /\ y e. B ) -> ( F ` y ) e. RR )
44 41 42 43 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> ( F ` y ) e. RR )
45 1 2 24 abvgt0 
 |-  ( ( F e. A /\ y e. B /\ y =/= ( 0g ` R ) ) -> 0 < ( F ` y ) )
46 45 3adant1r 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> 0 < ( F ` y ) )
47 44 46 elrpd 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> ( F ` y ) e. RR+ )
48 20 3ad2ant1 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> S e. RR )
49 47 48 rpcxpcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> ( ( F ` y ) ^c S ) e. RR+ )
50 49 rpgt0d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> 0 < ( ( F ` y ) ^c S ) )
51 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
52 51 oveq1d 
 |-  ( x = y -> ( ( F ` x ) ^c S ) = ( ( F ` y ) ^c S ) )
53 ovex 
 |-  ( ( F ` y ) ^c S ) e. _V
54 52 3 53 fvmpt 
 |-  ( y e. B -> ( G ` y ) = ( ( F ` y ) ^c S ) )
55 42 54 syl 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> ( G ` y ) = ( ( F ` y ) ^c S ) )
56 50 55 breqtrrd 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ y e. B /\ y =/= ( 0g ` R ) ) -> 0 < ( G ` y ) )
57 simp1l 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> F e. A )
58 simp2l 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> y e. B )
59 simp3l 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> z e. B )
60 eqid 
 |-  ( .r ` R ) = ( .r ` R )
61 1 2 60 abvmul 
 |-  ( ( F e. A /\ y e. B /\ z e. B ) -> ( F ` ( y ( .r ` R ) z ) ) = ( ( F ` y ) x. ( F ` z ) ) )
62 57 58 59 61 syl3anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( F ` ( y ( .r ` R ) z ) ) = ( ( F ` y ) x. ( F ` z ) ) )
63 62 oveq1d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` ( y ( .r ` R ) z ) ) ^c S ) = ( ( ( F ` y ) x. ( F ` z ) ) ^c S ) )
64 57 58 43 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( F ` y ) e. RR )
65 1 2 abvge0 
 |-  ( ( F e. A /\ y e. B ) -> 0 <_ ( F ` y ) )
66 57 58 65 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> 0 <_ ( F ` y ) )
67 1 2 abvcl 
 |-  ( ( F e. A /\ z e. B ) -> ( F ` z ) e. RR )
68 57 59 67 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( F ` z ) e. RR )
69 1 2 abvge0 
 |-  ( ( F e. A /\ z e. B ) -> 0 <_ ( F ` z ) )
70 57 59 69 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> 0 <_ ( F ` z ) )
71 35 3ad2ant1 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> S e. CC )
72 64 66 68 70 71 mulcxpd 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( ( F ` y ) x. ( F ` z ) ) ^c S ) = ( ( ( F ` y ) ^c S ) x. ( ( F ` z ) ^c S ) ) )
73 63 72 eqtrd 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` ( y ( .r ` R ) z ) ) ^c S ) = ( ( ( F ` y ) ^c S ) x. ( ( F ` z ) ^c S ) ) )
74 10 3ad2ant1 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> R e. Ring )
75 2 60 ringcl 
 |-  ( ( R e. Ring /\ y e. B /\ z e. B ) -> ( y ( .r ` R ) z ) e. B )
76 74 58 59 75 syl3anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) e. B )
77 fveq2 
 |-  ( x = ( y ( .r ` R ) z ) -> ( F ` x ) = ( F ` ( y ( .r ` R ) z ) ) )
78 77 oveq1d 
 |-  ( x = ( y ( .r ` R ) z ) -> ( ( F ` x ) ^c S ) = ( ( F ` ( y ( .r ` R ) z ) ) ^c S ) )
79 ovex 
 |-  ( ( F ` ( y ( .r ` R ) z ) ) ^c S ) e. _V
80 78 3 79 fvmpt 
 |-  ( ( y ( .r ` R ) z ) e. B -> ( G ` ( y ( .r ` R ) z ) ) = ( ( F ` ( y ( .r ` R ) z ) ) ^c S ) )
81 76 80 syl 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( G ` ( y ( .r ` R ) z ) ) = ( ( F ` ( y ( .r ` R ) z ) ) ^c S ) )
82 58 54 syl 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( G ` y ) = ( ( F ` y ) ^c S ) )
83 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
84 83 oveq1d 
 |-  ( x = z -> ( ( F ` x ) ^c S ) = ( ( F ` z ) ^c S ) )
85 ovex 
 |-  ( ( F ` z ) ^c S ) e. _V
86 84 3 85 fvmpt 
 |-  ( z e. B -> ( G ` z ) = ( ( F ` z ) ^c S ) )
87 59 86 syl 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( G ` z ) = ( ( F ` z ) ^c S ) )
88 82 87 oveq12d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( G ` y ) x. ( G ` z ) ) = ( ( ( F ` y ) ^c S ) x. ( ( F ` z ) ^c S ) ) )
89 73 81 88 3eqtr4d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( G ` ( y ( .r ` R ) z ) ) = ( ( G ` y ) x. ( G ` z ) ) )
90 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
91 74 90 syl 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> R e. Grp )
92 eqid 
 |-  ( +g ` R ) = ( +g ` R )
93 2 92 grpcl 
 |-  ( ( R e. Grp /\ y e. B /\ z e. B ) -> ( y ( +g ` R ) z ) e. B )
94 91 58 59 93 syl3anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( y ( +g ` R ) z ) e. B )
95 1 2 abvcl 
 |-  ( ( F e. A /\ ( y ( +g ` R ) z ) e. B ) -> ( F ` ( y ( +g ` R ) z ) ) e. RR )
96 57 94 95 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( F ` ( y ( +g ` R ) z ) ) e. RR )
97 1 2 abvge0 
 |-  ( ( F e. A /\ ( y ( +g ` R ) z ) e. B ) -> 0 <_ ( F ` ( y ( +g ` R ) z ) ) )
98 57 94 97 syl2anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> 0 <_ ( F ` ( y ( +g ` R ) z ) ) )
99 19 3ad2ant1 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( S e. RR /\ 0 < S /\ S <_ 1 ) )
100 99 simp1d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> S e. RR )
101 96 98 100 recxpcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) e. RR )
102 64 68 readdcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` y ) + ( F ` z ) ) e. RR )
103 64 68 66 70 addge0d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> 0 <_ ( ( F ` y ) + ( F ` z ) ) )
104 102 103 100 recxpcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( ( F ` y ) + ( F ` z ) ) ^c S ) e. RR )
105 64 66 100 recxpcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` y ) ^c S ) e. RR )
106 68 70 100 recxpcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` z ) ^c S ) e. RR )
107 105 106 readdcld 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( ( F ` y ) ^c S ) + ( ( F ` z ) ^c S ) ) e. RR )
108 1 2 92 abvtri 
 |-  ( ( F e. A /\ y e. B /\ z e. B ) -> ( F ` ( y ( +g ` R ) z ) ) <_ ( ( F ` y ) + ( F ` z ) ) )
109 57 58 59 108 syl3anc 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( F ` ( y ( +g ` R ) z ) ) <_ ( ( F ` y ) + ( F ` z ) ) )
110 99 simp2d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> 0 < S )
111 100 110 elrpd 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> S e. RR+ )
112 96 98 102 103 111 cxple2d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` ( y ( +g ` R ) z ) ) <_ ( ( F ` y ) + ( F ` z ) ) <-> ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) <_ ( ( ( F ` y ) + ( F ` z ) ) ^c S ) ) )
113 109 112 mpbid 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) <_ ( ( ( F ` y ) + ( F ` z ) ) ^c S ) )
114 99 simp3d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> S <_ 1 )
115 64 66 68 70 111 114 cxpaddle 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( ( F ` y ) + ( F ` z ) ) ^c S ) <_ ( ( ( F ` y ) ^c S ) + ( ( F ` z ) ^c S ) ) )
116 101 104 107 113 115 letrd 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) <_ ( ( ( F ` y ) ^c S ) + ( ( F ` z ) ^c S ) ) )
117 fveq2 
 |-  ( x = ( y ( +g ` R ) z ) -> ( F ` x ) = ( F ` ( y ( +g ` R ) z ) ) )
118 117 oveq1d 
 |-  ( x = ( y ( +g ` R ) z ) -> ( ( F ` x ) ^c S ) = ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) )
119 ovex 
 |-  ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) e. _V
120 118 3 119 fvmpt 
 |-  ( ( y ( +g ` R ) z ) e. B -> ( G ` ( y ( +g ` R ) z ) ) = ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) )
121 94 120 syl 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( G ` ( y ( +g ` R ) z ) ) = ( ( F ` ( y ( +g ` R ) z ) ) ^c S ) )
122 82 87 oveq12d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( ( G ` y ) + ( G ` z ) ) = ( ( ( F ` y ) ^c S ) + ( ( F ` z ) ^c S ) ) )
123 116 121 122 3brtr4d 
 |-  ( ( ( F e. A /\ S e. ( 0 (,] 1 ) ) /\ ( y e. B /\ y =/= ( 0g ` R ) ) /\ ( z e. B /\ z =/= ( 0g ` R ) ) ) -> ( G ` ( y ( +g ` R ) z ) ) <_ ( ( G ` y ) + ( G ` z ) ) )
124 4 5 6 7 8 10 23 40 56 89 123 isabvd 
 |-  ( ( F e. A /\ S e. ( 0 (,] 1 ) ) -> G e. A )