Metamath Proof Explorer

Theorem itgabs

Description: The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgabs.1 
|- ( ( ph /\ x e. A ) -> B e. V )
itgabs.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion itgabs 
|- ( ph -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )

Proof

Step Hyp Ref Expression
1 itgabs.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgabs.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 1 2 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
4 3 cjcld 
 |-  ( ph -> ( * ` S. A B _d x ) e. CC )
5 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
6 2 5 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
7 6 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
8 7 ralrimiva 
 |-  ( ph -> A. x e. A B e. CC )
9 nfv 
 |-  F/ y B e. CC
10 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
11 10 nfel1 
 |-  F/ x [_ y / x ]_ B e. CC
12 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
13 12 eleq1d 
 |-  ( x = y -> ( B e. CC <-> [_ y / x ]_ B e. CC ) )
14 9 11 13 cbvralw 
 |-  ( A. x e. A B e. CC <-> A. y e. A [_ y / x ]_ B e. CC )
15 8 14 sylib 
 |-  ( ph -> A. y e. A [_ y / x ]_ B e. CC )
16 15 r19.21bi 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. CC )
17 nfcv 
 |-  F/_ y B
18 17 10 12 cbvmpt 
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
19 18 2 eqeltrrid 
 |-  ( ph -> ( y e. A |-> [_ y / x ]_ B ) e. L^1 )
20 4 16 19 iblmulc2 
 |-  ( ph -> ( y e. A |-> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. L^1 )
21 4 adantr 
 |-  ( ( ph /\ y e. A ) -> ( * ` S. A B _d x ) e. CC )
22 21 16 mulcld 
 |-  ( ( ph /\ y e. A ) -> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) e. CC )
23 22 iblcn 
 |-  ( ph -> ( ( y e. A |-> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. L^1 <-> ( ( y e. A |-> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 /\ ( y e. A |-> ( Im ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 ) ) )
24 20 23 mpbid 
 |-  ( ph -> ( ( y e. A |-> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 /\ ( y e. A |-> ( Im ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 ) )
25 24 simpld 
 |-  ( ph -> ( y e. A |-> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 )
26 ovexd 
 |-  ( ( ph /\ y e. A ) -> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) e. _V )
27 26 20 iblabs 
 |-  ( ph -> ( y e. A |-> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 )
28 22 recld 
 |-  ( ( ph /\ y e. A ) -> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. RR )
29 22 abscld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. RR )
30 22 releabsd 
 |-  ( ( ph /\ y e. A ) -> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) <_ ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) )
31 25 27 28 29 30 itgle 
 |-  ( ph -> S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y <_ S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
32 3 abscld 
 |-  ( ph -> ( abs ` S. A B _d x ) e. RR )
33 32 recnd 
 |-  ( ph -> ( abs ` S. A B _d x ) e. CC )
34 33 sqvald 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) )
35 3 absvalsqd 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = ( S. A B _d x x. ( * ` S. A B _d x ) ) )
36 3 4 mulcomd 
 |-  ( ph -> ( S. A B _d x x. ( * ` S. A B _d x ) ) = ( ( * ` S. A B _d x ) x. S. A B _d x ) )
37 12 17 10 cbvitg 
 |-  S. A B _d x = S. A [_ y / x ]_ B _d y
38 37 oveq2i 
 |-  ( ( * ` S. A B _d x ) x. S. A B _d x ) = ( ( * ` S. A B _d x ) x. S. A [_ y / x ]_ B _d y )
39 4 16 19 itgmulc2 
 |-  ( ph -> ( ( * ` S. A B _d x ) x. S. A [_ y / x ]_ B _d y ) = S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y )
40 38 39 eqtrid 
 |-  ( ph -> ( ( * ` S. A B _d x ) x. S. A B _d x ) = S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y )
41 35 36 40 3eqtrd 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y )
42 41 fveq2d 
 |-  ( ph -> ( Re ` ( ( abs ` S. A B _d x ) ^ 2 ) ) = ( Re ` S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y ) )
43 32 resqcld 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) e. RR )
44 43 rered 
 |-  ( ph -> ( Re ` ( ( abs ` S. A B _d x ) ^ 2 ) ) = ( ( abs ` S. A B _d x ) ^ 2 ) )
45 26 20 itgre 
 |-  ( ph -> ( Re ` S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y ) = S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
46 42 44 45 3eqtr3d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
47 34 46 eqtr3d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) = S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
48 12 fveq2d 
 |-  ( x = y -> ( abs ` B ) = ( abs ` [_ y / x ]_ B ) )
49 nfcv 
 |-  F/_ y ( abs ` B )
50 nfcv 
 |-  F/_ x abs
51 50 10 nffv 
 |-  F/_ x ( abs ` [_ y / x ]_ B )
52 48 49 51 cbvitg 
 |-  S. A ( abs ` B ) _d x = S. A ( abs ` [_ y / x ]_ B ) _d y
53 52 oveq2i 
 |-  ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) = ( ( abs ` S. A B _d x ) x. S. A ( abs ` [_ y / x ]_ B ) _d y )
54 16 abscld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` [_ y / x ]_ B ) e. RR )
55 16 19 iblabs 
 |-  ( ph -> ( y e. A |-> ( abs ` [_ y / x ]_ B ) ) e. L^1 )
56 33 54 55 itgmulc2 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. S. A ( abs ` [_ y / x ]_ B ) _d y ) = S. A ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) _d y )
57 21 16 absmuld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) = ( ( abs ` ( * ` S. A B _d x ) ) x. ( abs ` [_ y / x ]_ B ) ) )
58 3 adantr 
 |-  ( ( ph /\ y e. A ) -> S. A B _d x e. CC )
59 58 abscjd 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( * ` S. A B _d x ) ) = ( abs ` S. A B _d x ) )
60 59 oveq1d 
 |-  ( ( ph /\ y e. A ) -> ( ( abs ` ( * ` S. A B _d x ) ) x. ( abs ` [_ y / x ]_ B ) ) = ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) )
61 57 60 eqtrd 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) = ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) )
62 61 itgeq2dv 
 |-  ( ph -> S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y = S. A ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) _d y )
63 56 62 eqtr4d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. S. A ( abs ` [_ y / x ]_ B ) _d y ) = S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
64 53 63 eqtrid 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) = S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
65 31 47 64 3brtr4d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) )
66 65 adantr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) )
67 32 adantr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( abs ` S. A B _d x ) e. RR )
68 7 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
69 1 2 iblabs 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
70 68 69 itgrecl 
 |-  ( ph -> S. A ( abs ` B ) _d x e. RR )
71 70 adantr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> S. A ( abs ` B ) _d x e. RR )
72 simpr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> 0 < ( abs ` S. A B _d x ) )
73 lemul2 
 |-  ( ( ( abs ` S. A B _d x ) e. RR /\ S. A ( abs ` B ) _d x e. RR /\ ( ( abs ` S. A B _d x ) e. RR /\ 0 < ( abs ` S. A B _d x ) ) ) -> ( ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x <-> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) ) )
74 67 71 67 72 73 syl112anc 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x <-> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) ) )
75 66 74 mpbird 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )
76 75 ex 
 |-  ( ph -> ( 0 < ( abs ` S. A B _d x ) -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x ) )
77 7 absge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` B ) )
78 69 68 77 itgge0 
 |-  ( ph -> 0 <_ S. A ( abs ` B ) _d x )
79 breq1 
 |-  ( 0 = ( abs ` S. A B _d x ) -> ( 0 <_ S. A ( abs ` B ) _d x <-> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x ) )
80 78 79 syl5ibcom 
 |-  ( ph -> ( 0 = ( abs ` S. A B _d x ) -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x ) )
81 3 absge0d 
 |-  ( ph -> 0 <_ ( abs ` S. A B _d x ) )
82 0re 
 |-  0 e. RR
83 leloe 
 |-  ( ( 0 e. RR /\ ( abs ` S. A B _d x ) e. RR ) -> ( 0 <_ ( abs ` S. A B _d x ) <-> ( 0 < ( abs ` S. A B _d x ) \/ 0 = ( abs ` S. A B _d x ) ) ) )
84 82 32 83 sylancr 
 |-  ( ph -> ( 0 <_ ( abs ` S. A B _d x ) <-> ( 0 < ( abs ` S. A B _d x ) \/ 0 = ( abs ` S. A B _d x ) ) ) )
85 81 84 mpbid 
 |-  ( ph -> ( 0 < ( abs ` S. A B _d x ) \/ 0 = ( abs ` S. A B _d x ) ) )
86 76 80 85 mpjaod 
 |-  ( ph -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )