Metamath Proof Explorer


Theorem iblss

Description: A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses iblss.1 φAB
iblss.2 φAdomvol
iblss.3 φxBCV
iblss.4 φxBC𝐿1
Assertion iblss φxAC𝐿1

Proof

Step Hyp Ref Expression
1 iblss.1 φAB
2 iblss.2 φAdomvol
3 iblss.3 φxBCV
4 iblss.4 φxBC𝐿1
5 1 resmptd φxBCA=xAC
6 iblmbf xBC𝐿1xBCMblFn
7 4 6 syl φxBCMblFn
8 mbfres xBCMblFnAdomvolxBCAMblFn
9 7 2 8 syl2anc φxBCAMblFn
10 5 9 eqeltrrd φxACMblFn
11 ifan ifxA0CikCik0=ifxAif0CikCik00
12 1 sselda φxAxB
13 12 ad4ant14 φk03xxAxB
14 7 3 mbfmptcl φxBC
15 14 ad4ant14 φk03xxBC
16 ax-icn i
17 ine0 i0
18 elfzelz k03k
19 18 ad3antlr φk03xxBk
20 expclz ii0kik
21 16 17 19 20 mp3an12i φk03xxBik
22 expne0i ii0kik0
23 16 17 19 22 mp3an12i φk03xxBik0
24 15 21 23 divcld φk03xxBCik
25 24 recld φk03xxBCik
26 0re 0
27 ifcl Cik0if0CikCik0
28 25 26 27 sylancl φk03xxBif0CikCik0
29 28 rexrd φk03xxBif0CikCik0*
30 max1 0Cik0if0CikCik0
31 26 25 30 sylancr φk03xxB0if0CikCik0
32 elxrge0 if0CikCik00+∞if0CikCik0*0if0CikCik0
33 29 31 32 sylanbrc φk03xxBif0CikCik00+∞
34 13 33 syldan φk03xxAif0CikCik00+∞
35 0e0iccpnf 00+∞
36 35 a1i φk03x¬xA00+∞
37 34 36 ifclda φk03xifxAif0CikCik000+∞
38 11 37 eqeltrid φk03xifxA0CikCik00+∞
39 38 fmpttd φk03xifxA0CikCik0:0+∞
40 eqidd φxifxB0CikCik0=xifxB0CikCik0
41 eqidd φxBCik=Cik
42 40 41 4 3 iblitg φk2xifxB0CikCik0
43 18 42 sylan2 φk032xifxB0CikCik0
44 ifan ifxB0CikCik0=ifxBif0CikCik00
45 35 a1i φk03x¬xB00+∞
46 33 45 ifclda φk03xifxBif0CikCik000+∞
47 44 46 eqeltrid φk03xifxB0CikCik00+∞
48 47 fmpttd φk03xifxB0CikCik0:0+∞
49 28 leidd φk03xxBif0CikCik0if0CikCik0
50 breq1 if0CikCik0=ifxAif0CikCik00if0CikCik0if0CikCik0ifxAif0CikCik00if0CikCik0
51 breq1 0=ifxAif0CikCik000if0CikCik0ifxAif0CikCik00if0CikCik0
52 50 51 ifboth if0CikCik0if0CikCik00if0CikCik0ifxAif0CikCik00if0CikCik0
53 49 31 52 syl2anc φk03xxBifxAif0CikCik00if0CikCik0
54 iftrue xBifxBif0CikCik00=if0CikCik0
55 54 adantl φk03xxBifxBif0CikCik00=if0CikCik0
56 53 55 breqtrrd φk03xxBifxAif0CikCik00ifxBif0CikCik00
57 0le0 00
58 57 a1i φk03x¬xB00
59 13 stoic1a φk03x¬xB¬xA
60 59 iffalsed φk03x¬xBifxAif0CikCik00=0
61 iffalse ¬xBifxBif0CikCik00=0
62 61 adantl φk03x¬xBifxBif0CikCik00=0
63 58 60 62 3brtr4d φk03x¬xBifxAif0CikCik00ifxBif0CikCik00
64 56 63 pm2.61dan φk03xifxAif0CikCik00ifxBif0CikCik00
65 64 11 44 3brtr4g φk03xifxA0CikCik0ifxB0CikCik0
66 65 ralrimiva φk03xifxA0CikCik0ifxB0CikCik0
67 reex V
68 67 a1i φk03V
69 eqidd φk03xifxA0CikCik0=xifxA0CikCik0
70 eqidd φk03xifxB0CikCik0=xifxB0CikCik0
71 68 38 47 69 70 ofrfval2 φk03xifxA0CikCik0fxifxB0CikCik0xifxA0CikCik0ifxB0CikCik0
72 66 71 mpbird φk03xifxA0CikCik0fxifxB0CikCik0
73 itg2le xifxA0CikCik0:0+∞xifxB0CikCik0:0+∞xifxA0CikCik0fxifxB0CikCik02xifxA0CikCik02xifxB0CikCik0
74 39 48 72 73 syl3anc φk032xifxA0CikCik02xifxB0CikCik0
75 itg2lecl xifxA0CikCik0:0+∞2xifxB0CikCik02xifxA0CikCik02xifxB0CikCik02xifxA0CikCik0
76 39 43 74 75 syl3anc φk032xifxA0CikCik0
77 76 ralrimiva φk032xifxA0CikCik0
78 eqidd φxifxA0CikCik0=xifxA0CikCik0
79 eqidd φxACik=Cik
80 12 14 syldan φxAC
81 78 79 80 isibl2 φxAC𝐿1xACMblFnk032xifxA0CikCik0
82 10 77 81 mpbir2and φxAC𝐿1