Metamath Proof Explorer

Theorem itgabs

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

Ref Expression
Hypotheses itgabs.1 ⊢φ∧x∈A→B∈V
itgabs.2 ⊢φ→x∈A⟼B∈𝐿1
Assertion itgabs ⊢φ→∫ABdx≤∫ABdx

Proof

Step Hyp Ref Expression
1 itgabs.1 ⊢φ∧x∈A→B∈V
2 itgabs.2 ⊢φ→x∈A⟼B∈𝐿1
3 1 2 itgcl ⊢φ→∫ABdx∈ℂ
4 3 cjcld ⊢φ→∫ABdx‾∈ℂ
5 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
6 2 5 syl ⊢φ→x∈A⟼B∈MblFn
7 6 1 mbfmptcl ⊢φ∧x∈A→B∈ℂ
8 7 ralrimiva ⊢φ→∀x∈AB∈ℂ
9 nfv ⊢ℲyB∈ℂ
10 nfcsb1v ⊢Ⅎ_x⦋y/x⦌B
11 10 nfel1 ⊢Ⅎx⦋y/x⦌B∈ℂ
12 csbeq1a ⊢x=y→B=⦋y/x⦌B
13 12 eleq1d ⊢x=y→B∈ℂ↔⦋y/x⦌B∈ℂ
14 9 11 13 cbvralw ⊢∀x∈AB∈ℂ↔∀y∈A⦋y/x⦌B∈ℂ
15 8 14 sylib ⊢φ→∀y∈A⦋y/x⦌B∈ℂ
16 15 r19.21bi ⊢φ∧y∈A→⦋y/x⦌B∈ℂ
17 nfcv ⊢Ⅎ_yB
18 17 10 12 cbvmpt ⊢x∈A⟼B=y∈A⟼⦋y/x⦌B
19 18 2 eqeltrrid ⊢φ→y∈A⟼⦋y/x⦌B∈𝐿1
20 4 16 19 iblmulc2 ⊢φ→y∈A⟼∫ABdx‾⁢⦋y/x⦌B∈𝐿1
21 4 adantr ⊢φ∧y∈A→∫ABdx‾∈ℂ
22 21 16 mulcld ⊢φ∧y∈A→∫ABdx‾⁢⦋y/x⦌B∈ℂ
23 22 iblcn ⊢φ→y∈A⟼∫ABdx‾⁢⦋y/x⦌B∈𝐿1↔y∈A⟼ℜ⁡∫ABdx‾⁢⦋y/x⦌B∈𝐿1∧y∈A⟼ℑ⁡∫ABdx‾⁢⦋y/x⦌B∈𝐿1
24 20 23 mpbid ⊢φ→y∈A⟼ℜ⁡∫ABdx‾⁢⦋y/x⦌B∈𝐿1∧y∈A⟼ℑ⁡∫ABdx‾⁢⦋y/x⦌B∈𝐿1
25 24 simpld ⊢φ→y∈A⟼ℜ⁡∫ABdx‾⁢⦋y/x⦌B∈𝐿1
26 ovexd ⊢φ∧y∈A→∫ABdx‾⁢⦋y/x⦌B∈V
27 26 20 iblabs ⊢φ→y∈A⟼∫ABdx‾⁢⦋y/x⦌B∈𝐿1
28 22 recld ⊢φ∧y∈A→ℜ⁡∫ABdx‾⁢⦋y/x⦌B∈ℝ
29 22 abscld ⊢φ∧y∈A→∫ABdx‾⁢⦋y/x⦌B∈ℝ
30 22 releabsd ⊢φ∧y∈A→ℜ⁡∫ABdx‾⁢⦋y/x⦌B≤∫ABdx‾⁢⦋y/x⦌B
31 25 27 28 29 30 itgle ⊢φ→∫Aℜ⁡∫ABdx‾⁢⦋y/x⦌Bdy≤∫A∫ABdx‾⁢⦋y/x⦌Bdy
32 3 abscld ⊢φ→∫ABdx∈ℝ
33 32 recnd ⊢φ→∫ABdx∈ℂ
34 33 sqvald ⊢φ→∫ABdx2=∫ABdx⁢∫ABdx
35 3 absvalsqd ⊢φ→∫ABdx2=∫ABdx⁢∫ABdx‾
36 3 4 mulcomd ⊢φ→∫ABdx⁢∫ABdx‾=∫ABdx‾⁢∫ABdx
37 12 17 10 cbvitg ⊢∫ABdx=∫A⦋y/x⦌Bdy
38 37 oveq2i ⊢∫ABdx‾⁢∫ABdx=∫ABdx‾⁢∫A⦋y/x⦌Bdy
39 4 16 19 itgmulc2 ⊢φ→∫ABdx‾⁢∫A⦋y/x⦌Bdy=∫A∫ABdx‾⁢⦋y/x⦌Bdy
40 38 39 eqtrid ⊢φ→∫ABdx‾⁢∫ABdx=∫A∫ABdx‾⁢⦋y/x⦌Bdy
41 35 36 40 3eqtrd ⊢φ→∫ABdx2=∫A∫ABdx‾⁢⦋y/x⦌Bdy
42 41 fveq2d ⊢φ→ℜ⁡∫ABdx2=ℜ⁡∫A∫ABdx‾⁢⦋y/x⦌Bdy
43 32 resqcld ⊢φ→∫ABdx2∈ℝ
44 43 rered ⊢φ→ℜ⁡∫ABdx2=∫ABdx2
45 26 20 itgre ⊢φ→ℜ⁡∫A∫ABdx‾⁢⦋y/x⦌Bdy=∫Aℜ⁡∫ABdx‾⁢⦋y/x⦌Bdy
46 42 44 45 3eqtr3d ⊢φ→∫ABdx2=∫Aℜ⁡∫ABdx‾⁢⦋y/x⦌Bdy
47 34 46 eqtr3d ⊢φ→∫ABdx⁢∫ABdx=∫Aℜ⁡∫ABdx‾⁢⦋y/x⦌Bdy
48 12 fveq2d ⊢x=y→B=⦋y/x⦌B
49 nfcv ⊢Ⅎ_yB
50 nfcv ⊢Ⅎ_xabs
51 50 10 nffv ⊢Ⅎ_x⦋y/x⦌B
52 48 49 51 cbvitg ⊢∫ABdx=∫A⦋y/x⦌Bdy
53 52 oveq2i ⊢∫ABdx⁢∫ABdx=∫ABdx⁢∫A⦋y/x⦌Bdy
54 16 abscld ⊢φ∧y∈A→⦋y/x⦌B∈ℝ
55 16 19 iblabs ⊢φ→y∈A⟼⦋y/x⦌B∈𝐿1
56 33 54 55 itgmulc2 ⊢φ→∫ABdx⁢∫A⦋y/x⦌Bdy=∫A∫ABdx⁢⦋y/x⦌Bdy
57 21 16 absmuld ⊢φ∧y∈A→∫ABdx‾⁢⦋y/x⦌B=∫ABdx‾⁢⦋y/x⦌B
58 3 adantr ⊢φ∧y∈A→∫ABdx∈ℂ
59 58 abscjd ⊢φ∧y∈A→∫ABdx‾=∫ABdx
60 59 oveq1d ⊢φ∧y∈A→∫ABdx‾⁢⦋y/x⦌B=∫ABdx⁢⦋y/x⦌B
61 57 60 eqtrd ⊢φ∧y∈A→∫ABdx‾⁢⦋y/x⦌B=∫ABdx⁢⦋y/x⦌B
62 61 itgeq2dv ⊢φ→∫A∫ABdx‾⁢⦋y/x⦌Bdy=∫A∫ABdx⁢⦋y/x⦌Bdy
63 56 62 eqtr4d ⊢φ→∫ABdx⁢∫A⦋y/x⦌Bdy=∫A∫ABdx‾⁢⦋y/x⦌Bdy
64 53 63 eqtrid ⊢φ→∫ABdx⁢∫ABdx=∫A∫ABdx‾⁢⦋y/x⦌Bdy
65 31 47 64 3brtr4d ⊢φ→∫ABdx⁢∫ABdx≤∫ABdx⁢∫ABdx
66 65 adantr ⊢φ∧0<∫ABdx→∫ABdx⁢∫ABdx≤∫ABdx⁢∫ABdx
67 32 adantr ⊢φ∧0<∫ABdx→∫ABdx∈ℝ
68 7 abscld ⊢φ∧x∈A→B∈ℝ
69 1 2 iblabs ⊢φ→x∈A⟼B∈𝐿1
70 68 69 itgrecl ⊢φ→∫ABdx∈ℝ
71 70 adantr ⊢φ∧0<∫ABdx→∫ABdx∈ℝ
72 simpr ⊢φ∧0<∫ABdx→0<∫ABdx
73 lemul2 ⊢∫ABdx∈ℝ∧∫ABdx∈ℝ∧∫ABdx∈ℝ∧0<∫ABdx→∫ABdx≤∫ABdx↔∫ABdx⁢∫ABdx≤∫ABdx⁢∫ABdx
74 67 71 67 72 73 syl112anc ⊢φ∧0<∫ABdx→∫ABdx≤∫ABdx↔∫ABdx⁢∫ABdx≤∫ABdx⁢∫ABdx
75 66 74 mpbird ⊢φ∧0<∫ABdx→∫ABdx≤∫ABdx
76 75 ex ⊢φ→0<∫ABdx→∫ABdx≤∫ABdx
77 7 absge0d ⊢φ∧x∈A→0≤B
78 69 68 77 itgge0 ⊢φ→0≤∫ABdx
79 breq1 ⊢0=∫ABdx→0≤∫ABdx↔∫ABdx≤∫ABdx
80 78 79 syl5ibcom ⊢φ→0=∫ABdx→∫ABdx≤∫ABdx
81 3 absge0d ⊢φ→0≤∫ABdx
82 0re ⊢0∈ℝ
83 leloe ⊢0∈ℝ∧∫ABdx∈ℝ→0≤∫ABdx↔0<∫ABdx∨0=∫ABdx
84 82 32 83 sylancr ⊢φ→0≤∫ABdx↔0<∫ABdx∨0=∫ABdx
85 81 84 mpbid ⊢φ→0<∫ABdx∨0=∫ABdx
86 76 80 85 mpjaod ⊢φ→∫ABdx≤∫ABdx