Metamath Proof Explorer

Theorem ftc1anclem4

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 17-Jun-2018)

Ref Expression
Assertion ftc1anclem4 
|- ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 ffvelcdm 
 |-  ( ( G : RR --> RR /\ t e. RR ) -> ( G ` t ) e. RR )
2 1 recnd 
 |-  ( ( G : RR --> RR /\ t e. RR ) -> ( G ` t ) e. CC )
3 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
4 3 ffvelcdmda 
 |-  ( ( F e. dom S.1 /\ t e. RR ) -> ( F ` t ) e. RR )
5 4 recnd 
 |-  ( ( F e. dom S.1 /\ t e. RR ) -> ( F ` t ) e. CC )
6 subcl 
 |-  ( ( ( G ` t ) e. CC /\ ( F ` t ) e. CC ) -> ( ( G ` t ) - ( F ` t ) ) e. CC )
7 2 5 6 syl2anr 
 |-  ( ( ( F e. dom S.1 /\ t e. RR ) /\ ( G : RR --> RR /\ t e. RR ) ) -> ( ( G ` t ) - ( F ` t ) ) e. CC )
8 7 anandirs 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( ( G ` t ) - ( F ` t ) ) e. CC )
9 8 abscld 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) e. RR )
10 9 rexrd 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) e. RR* )
11 8 absge0d 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> 0 <_ ( abs ` ( ( G ` t ) - ( F ` t ) ) ) )
12 elxrge0 
 |-  ( ( abs ` ( ( G ` t ) - ( F ` t ) ) ) e. ( 0 [,] +oo ) <-> ( ( abs ` ( ( G ` t ) - ( F ` t ) ) ) e. RR* /\ 0 <_ ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) )
13 10 11 12 sylanbrc 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) e. ( 0 [,] +oo ) )
14 13 fmpttd 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) )
15 14 3adant2 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) )
16 reex 
 |-  RR e. _V
17 16 a1i 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> RR e. _V )
18 fvexd 
 |-  ( ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( G ` t ) ) e. _V )
19 fvexd 
 |-  ( ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( F ` t ) ) e. _V )
20 eqidd 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( G ` t ) ) ) = ( t e. RR |-> ( abs ` ( G ` t ) ) ) )
21 eqidd 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( F ` t ) ) ) = ( t e. RR |-> ( abs ` ( F ` t ) ) ) )
22 17 18 19 20 21 offval2 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( ( t e. RR |-> ( abs ` ( G ` t ) ) ) oF + ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) = ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) )
23 22 fveq2d 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( ( t e. RR |-> ( abs ` ( G ` t ) ) ) oF + ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) ) = ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) )
24 id 
 |-  ( G : RR --> RR -> G : RR --> RR )
25 24 feqmptd 
 |-  ( G : RR --> RR -> G = ( t e. RR |-> ( G ` t ) ) )
26 absf 
 |-  abs : CC --> RR
27 26 a1i 
 |-  ( G : RR --> RR -> abs : CC --> RR )
28 27 feqmptd 
 |-  ( G : RR --> RR -> abs = ( x e. CC |-> ( abs ` x ) ) )
29 fveq2 
 |-  ( x = ( G ` t ) -> ( abs ` x ) = ( abs ` ( G ` t ) ) )
30 2 25 28 29 fmptco 
 |-  ( G : RR --> RR -> ( abs o. G ) = ( t e. RR |-> ( abs ` ( G ` t ) ) ) )
31 30 adantl 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( abs o. G ) = ( t e. RR |-> ( abs ` ( G ` t ) ) ) )
32 iblmbf 
 |-  ( G e. L^1 -> G e. MblFn )
33 ftc1anclem1 
 |-  ( ( G : RR --> RR /\ G e. MblFn ) -> ( abs o. G ) e. MblFn )
34 32 33 sylan2 
 |-  ( ( G : RR --> RR /\ G e. L^1 ) -> ( abs o. G ) e. MblFn )
35 34 ancoms 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( abs o. G ) e. MblFn )
36 31 35 eqeltrrd 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( G ` t ) ) ) e. MblFn )
37 36 3adant1 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( G ` t ) ) ) e. MblFn )
38 2 abscld 
 |-  ( ( G : RR --> RR /\ t e. RR ) -> ( abs ` ( G ` t ) ) e. RR )
39 2 absge0d 
 |-  ( ( G : RR --> RR /\ t e. RR ) -> 0 <_ ( abs ` ( G ` t ) ) )
40 elrege0 
 |-  ( ( abs ` ( G ` t ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( G ` t ) ) e. RR /\ 0 <_ ( abs ` ( G ` t ) ) ) )
41 38 39 40 sylanbrc 
 |-  ( ( G : RR --> RR /\ t e. RR ) -> ( abs ` ( G ` t ) ) e. ( 0 [,) +oo ) )
42 41 fmpttd 
 |-  ( G : RR --> RR -> ( t e. RR |-> ( abs ` ( G ` t ) ) ) : RR --> ( 0 [,) +oo ) )
43 42 3ad2ant3 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( G ` t ) ) ) : RR --> ( 0 [,) +oo ) )
44 iftrue 
 |-  ( t e. RR -> if ( t e. RR , ( abs ` ( G ` t ) ) , 0 ) = ( abs ` ( G ` t ) ) )
45 44 mpteq2ia 
 |-  ( t e. RR |-> if ( t e. RR , ( abs ` ( G ` t ) ) , 0 ) ) = ( t e. RR |-> ( abs ` ( G ` t ) ) )
46 45 fveq2i 
 |-  ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( G ` t ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( G ` t ) ) ) )
47 1 adantll 
 |-  ( ( ( G e. L^1 /\ G : RR --> RR ) /\ t e. RR ) -> ( G ` t ) e. RR )
48 simpr 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> G : RR --> RR )
49 48 feqmptd 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> G = ( t e. RR |-> ( G ` t ) ) )
50 simpl 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> G e. L^1 )
51 49 50 eqeltrrd 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( G ` t ) ) e. L^1 )
52 47 51 36 iblabsnc 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( G ` t ) ) ) e. L^1 )
53 38 adantll 
 |-  ( ( ( G e. L^1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( G ` t ) ) e. RR )
54 39 adantll 
 |-  ( ( ( G e. L^1 /\ G : RR --> RR ) /\ t e. RR ) -> 0 <_ ( abs ` ( G ` t ) ) )
55 53 54 iblpos 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( ( t e. RR |-> ( abs ` ( G ` t ) ) ) e. L^1 <-> ( ( t e. RR |-> ( abs ` ( G ` t ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( G ` t ) ) , 0 ) ) ) e. RR ) ) )
56 52 55 mpbid 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( ( t e. RR |-> ( abs ` ( G ` t ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( G ` t ) ) , 0 ) ) ) e. RR ) )
57 56 simprd 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( G ` t ) ) , 0 ) ) ) e. RR )
58 46 57 eqeltrrid 
 |-  ( ( G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( G ` t ) ) ) ) e. RR )
59 58 3adant1 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( G ` t ) ) ) ) e. RR )
60 5 abscld 
 |-  ( ( F e. dom S.1 /\ t e. RR ) -> ( abs ` ( F ` t ) ) e. RR )
61 5 absge0d 
 |-  ( ( F e. dom S.1 /\ t e. RR ) -> 0 <_ ( abs ` ( F ` t ) ) )
62 elrege0 
 |-  ( ( abs ` ( F ` t ) ) e. ( 0 [,) +oo ) <-> ( ( abs ` ( F ` t ) ) e. RR /\ 0 <_ ( abs ` ( F ` t ) ) ) )
63 60 61 62 sylanbrc 
 |-  ( ( F e. dom S.1 /\ t e. RR ) -> ( abs ` ( F ` t ) ) e. ( 0 [,) +oo ) )
64 63 fmpttd 
 |-  ( F e. dom S.1 -> ( t e. RR |-> ( abs ` ( F ` t ) ) ) : RR --> ( 0 [,) +oo ) )
65 64 3ad2ant1 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( F ` t ) ) ) : RR --> ( 0 [,) +oo ) )
66 iftrue 
 |-  ( t e. RR -> if ( t e. RR , ( abs ` ( F ` t ) ) , 0 ) = ( abs ` ( F ` t ) ) )
67 66 mpteq2ia 
 |-  ( t e. RR |-> if ( t e. RR , ( abs ` ( F ` t ) ) , 0 ) ) = ( t e. RR |-> ( abs ` ( F ` t ) ) )
68 67 fveq2i 
 |-  ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( F ` t ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> ( abs ` ( F ` t ) ) ) )
69 3 feqmptd 
 |-  ( F e. dom S.1 -> F = ( t e. RR |-> ( F ` t ) ) )
70 i1fibl 
 |-  ( F e. dom S.1 -> F e. L^1 )
71 69 70 eqeltrrd 
 |-  ( F e. dom S.1 -> ( t e. RR |-> ( F ` t ) ) e. L^1 )
72 26 a1i 
 |-  ( F e. dom S.1 -> abs : CC --> RR )
73 72 feqmptd 
 |-  ( F e. dom S.1 -> abs = ( x e. CC |-> ( abs ` x ) ) )
74 fveq2 
 |-  ( x = ( F ` t ) -> ( abs ` x ) = ( abs ` ( F ` t ) ) )
75 5 69 73 74 fmptco 
 |-  ( F e. dom S.1 -> ( abs o. F ) = ( t e. RR |-> ( abs ` ( F ` t ) ) ) )
76 i1fmbf 
 |-  ( F e. dom S.1 -> F e. MblFn )
77 ftc1anclem1 
 |-  ( ( F : RR --> RR /\ F e. MblFn ) -> ( abs o. F ) e. MblFn )
78 3 76 77 syl2anc 
 |-  ( F e. dom S.1 -> ( abs o. F ) e. MblFn )
79 75 78 eqeltrrd 
 |-  ( F e. dom S.1 -> ( t e. RR |-> ( abs ` ( F ` t ) ) ) e. MblFn )
80 4 71 79 iblabsnc 
 |-  ( F e. dom S.1 -> ( t e. RR |-> ( abs ` ( F ` t ) ) ) e. L^1 )
81 60 61 iblpos 
 |-  ( F e. dom S.1 -> ( ( t e. RR |-> ( abs ` ( F ` t ) ) ) e. L^1 <-> ( ( t e. RR |-> ( abs ` ( F ` t ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR ) ) )
82 80 81 mpbid 
 |-  ( F e. dom S.1 -> ( ( t e. RR |-> ( abs ` ( F ` t ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR ) )
83 82 simprd 
 |-  ( F e. dom S.1 -> ( S.2 ` ( t e. RR |-> if ( t e. RR , ( abs ` ( F ` t ) ) , 0 ) ) ) e. RR )
84 68 83 eqeltrrid 
 |-  ( F e. dom S.1 -> ( S.2 ` ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) e. RR )
85 84 3ad2ant1 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) e. RR )
86 37 43 59 65 85 itg2addnc 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( ( t e. RR |-> ( abs ` ( G ` t ) ) ) oF + ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) ) = ( ( S.2 ` ( t e. RR |-> ( abs ` ( G ` t ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) ) )
87 23 86 eqtr3d 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) = ( ( S.2 ` ( t e. RR |-> ( abs ` ( G ` t ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) ) )
88 59 85 readdcld 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( ( S.2 ` ( t e. RR |-> ( abs ` ( G ` t ) ) ) ) + ( S.2 ` ( t e. RR |-> ( abs ` ( F ` t ) ) ) ) ) e. RR )
89 87 88 eqeltrd 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) e. RR )
90 readdcl 
 |-  ( ( ( abs ` ( G ` t ) ) e. RR /\ ( abs ` ( F ` t ) ) e. RR ) -> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. RR )
91 38 60 90 syl2anr 
 |-  ( ( ( F e. dom S.1 /\ t e. RR ) /\ ( G : RR --> RR /\ t e. RR ) ) -> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. RR )
92 91 anandirs 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. RR )
93 92 rexrd 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. RR* )
94 38 adantll 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( G ` t ) ) e. RR )
95 60 adantlr 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( F ` t ) ) e. RR )
96 39 adantll 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> 0 <_ ( abs ` ( G ` t ) ) )
97 61 adantlr 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> 0 <_ ( abs ` ( F ` t ) ) )
98 94 95 96 97 addge0d 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> 0 <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) )
99 elxrge0 
 |-  ( ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. ( 0 [,] +oo ) <-> ( ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. RR* /\ 0 <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) )
100 93 98 99 sylanbrc 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) e. ( 0 [,] +oo ) )
101 100 fmpttd 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) )
102 101 3adant2 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) )
103 abs2dif2 
 |-  ( ( ( G ` t ) e. CC /\ ( F ` t ) e. CC ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) )
104 2 5 103 syl2anr 
 |-  ( ( ( F e. dom S.1 /\ t e. RR ) /\ ( G : RR --> RR /\ t e. RR ) ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) )
105 104 anandirs 
 |-  ( ( ( F e. dom S.1 /\ G : RR --> RR ) /\ t e. RR ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) )
106 105 ralrimiva 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> A. t e. RR ( abs ` ( ( G ` t ) - ( F ` t ) ) ) <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) )
107 16 a1i 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> RR e. _V )
108 eqidd 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) = ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) )
109 eqidd 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) = ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) )
110 107 9 92 108 109 ofrfval2 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> ( ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) oR <_ ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) <-> A. t e. RR ( abs ` ( ( G ` t ) - ( F ` t ) ) ) <_ ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) )
111 106 110 mpbird 
 |-  ( ( F e. dom S.1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) oR <_ ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) )
112 111 3adant2 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) oR <_ ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) )
113 itg2le 
 |-  ( ( ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) /\ ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) /\ ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) oR <_ ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) ) <_ ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) )
114 15 102 112 113 syl3anc 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) ) <_ ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) )
115 itg2lecl 
 |-  ( ( ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) e. RR /\ ( S.2 ` ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) ) <_ ( S.2 ` ( t e. RR |-> ( ( abs ` ( G ` t ) ) + ( abs ` ( F ` t ) ) ) ) ) ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) ) e. RR )
116 15 89 114 115 syl3anc 
 |-  ( ( F e. dom S.1 /\ G e. L^1 /\ G : RR --> RR ) -> ( S.2 ` ( t e. RR |-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) ) ) e. RR )