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