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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 )