Metamath Proof Explorer


Theorem bddmulibl

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

Ref Expression
Assertion bddmulibl FMblFnG𝐿1xydomFFyxF×fG𝐿1

Proof

Step Hyp Ref Expression
1 mbff FMblFnF:domF
2 1 ad2antrr FMblFnG𝐿1xydomFFyxF:domF
3 2 ffnd FMblFnG𝐿1xydomFFyxFFndomF
4 iblmbf G𝐿1GMblFn
5 4 ad2antlr FMblFnG𝐿1xydomFFyxGMblFn
6 mbff GMblFnG:domG
7 5 6 syl FMblFnG𝐿1xydomFFyxG:domG
8 7 ffnd FMblFnG𝐿1xydomFFyxGFndomG
9 mbfdm FMblFndomFdomvol
10 9 ad2antrr FMblFnG𝐿1xydomFFyxdomFdomvol
11 mbfdm GMblFndomGdomvol
12 5 11 syl FMblFnG𝐿1xydomFFyxdomGdomvol
13 eqid domFdomG=domFdomG
14 eqidd FMblFnG𝐿1xydomFFyxzdomFFz=Fz
15 eqidd FMblFnG𝐿1xydomFFyxzdomGGz=Gz
16 3 8 10 12 13 14 15 offval FMblFnG𝐿1xydomFFyxF×fG=zdomFdomGFzGz
17 ovexd FMblFnG𝐿1xydomFFyxzdomFdomGFzGzV
18 simpll FMblFnG𝐿1xydomFFyxFMblFn
19 18 5 mbfmul FMblFnG𝐿1xydomFFyxF×fGMblFn
20 16 19 eqeltrrd FMblFnG𝐿1xydomFFyxzdomFdomGFzGzMblFn
21 absf abs:
22 21 a1i FMblFnG𝐿1xydomFFyxabs:
23 20 17 mbfmptcl FMblFnG𝐿1xydomFFyxzdomFdomGFzGz
24 22 23 cofmpt FMblFnG𝐿1xydomFFyxabszdomFdomGFzGz=zdomFdomGFzGz
25 23 fmpttd FMblFnG𝐿1xydomFFyxzdomFdomGFzGz:domFdomG
26 ax-resscn
27 ssid
28 cncfss cncn
29 26 27 28 mp2an cncn
30 abscncf abs:cn
31 29 30 sselii abs:cn
32 31 a1i FMblFnG𝐿1xydomFFyxabs:cn
33 cncombf zdomFdomGFzGzMblFnzdomFdomGFzGz:domFdomGabs:cnabszdomFdomGFzGzMblFn
34 20 25 32 33 syl3anc FMblFnG𝐿1xydomFFyxabszdomFdomGFzGzMblFn
35 24 34 eqeltrrd FMblFnG𝐿1xydomFFyxzdomFdomGFzGzMblFn
36 23 abscld FMblFnG𝐿1xydomFFyxzdomFdomGFzGz
37 36 rexrd FMblFnG𝐿1xydomFFyxzdomFdomGFzGz*
38 23 absge0d FMblFnG𝐿1xydomFFyxzdomFdomG0FzGz
39 elxrge0 FzGz0+∞FzGz*0FzGz
40 37 38 39 sylanbrc FMblFnG𝐿1xydomFFyxzdomFdomGFzGz0+∞
41 0e0iccpnf 00+∞
42 41 a1i FMblFnG𝐿1xydomFFyx¬zdomFdomG00+∞
43 40 42 ifclda FMblFnG𝐿1xydomFFyxifzdomFdomGFzGz00+∞
44 43 adantr FMblFnG𝐿1xydomFFyxzifzdomFdomGFzGz00+∞
45 44 fmpttd FMblFnG𝐿1xydomFFyxzifzdomFdomGFzGz0:0+∞
46 reex V
47 46 a1i FMblFnG𝐿1xydomFFyx¬domFdomG=V
48 simprl FMblFnG𝐿1xydomFFyxx
49 48 ad2antrr FMblFnG𝐿1xydomFFyx¬domFdomG=zx
50 elinel2 zdomFdomGzdomG
51 ffvelrn G:domGzdomGGz
52 7 50 51 syl2an FMblFnG𝐿1xydomFFyxzdomFdomGGz
53 52 abscld FMblFnG𝐿1xydomFFyxzdomFdomGGz
54 52 absge0d FMblFnG𝐿1xydomFFyxzdomFdomG0Gz
55 elrege0 Gz0+∞Gz0Gz
56 53 54 55 sylanbrc FMblFnG𝐿1xydomFFyxzdomFdomGGz0+∞
57 0e0icopnf 00+∞
58 57 a1i FMblFnG𝐿1xydomFFyx¬zdomFdomG00+∞
59 56 58 ifclda FMblFnG𝐿1xydomFFyxifzdomFdomGGz00+∞
60 59 ad2antrr FMblFnG𝐿1xydomFFyx¬domFdomG=zifzdomFdomGGz00+∞
61 fconstmpt ×x=zx
62 61 a1i FMblFnG𝐿1xydomFFyx¬domFdomG=×x=zx
63 eqidd FMblFnG𝐿1xydomFFyx¬domFdomG=zifzdomFdomGGz0=zifzdomFdomGGz0
64 47 49 60 62 63 offval2 FMblFnG𝐿1xydomFFyx¬domFdomG=×x×fzifzdomFdomGGz0=zxifzdomFdomGGz0
65 ovif2 xifzdomFdomGGz0=ifzdomFdomGxGzx0
66 48 recnd FMblFnG𝐿1xydomFFyxx
67 66 adantr FMblFnG𝐿1xydomFFyx¬domFdomG=x
68 67 mul01d FMblFnG𝐿1xydomFFyx¬domFdomG=x0=0
69 68 ifeq2d FMblFnG𝐿1xydomFFyx¬domFdomG=ifzdomFdomGxGzx0=ifzdomFdomGxGz0
70 65 69 eqtrid FMblFnG𝐿1xydomFFyx¬domFdomG=xifzdomFdomGGz0=ifzdomFdomGxGz0
71 70 mpteq2dv FMblFnG𝐿1xydomFFyx¬domFdomG=zxifzdomFdomGGz0=zifzdomFdomGxGz0
72 64 71 eqtrd FMblFnG𝐿1xydomFFyx¬domFdomG=×x×fzifzdomFdomGGz0=zifzdomFdomGxGz0
73 72 fveq2d FMblFnG𝐿1xydomFFyx¬domFdomG=2×x×fzifzdomFdomGGz0=2zifzdomFdomGxGz0
74 59 adantr FMblFnG𝐿1xydomFFyxzifzdomFdomGGz00+∞
75 74 fmpttd FMblFnG𝐿1xydomFFyxzifzdomFdomGGz0:0+∞
76 75 adantr FMblFnG𝐿1xydomFFyx¬domFdomG=zifzdomFdomGGz0:0+∞
77 inss2 domFdomGdomG
78 77 a1i FMblFnG𝐿1xydomFFyxdomFdomGdomG
79 20 17 mbfdm2 FMblFnG𝐿1xydomFFyxdomFdomGdomvol
80 7 ffvelrnda FMblFnG𝐿1xydomFFyxzdomGGz
81 7 feqmptd FMblFnG𝐿1xydomFFyxG=zdomGGz
82 simplr FMblFnG𝐿1xydomFFyxG𝐿1
83 81 82 eqeltrrd FMblFnG𝐿1xydomFFyxzdomGGz𝐿1
84 78 79 80 83 iblss FMblFnG𝐿1xydomFFyxzdomFdomGGz𝐿1
85 52 84 iblabs FMblFnG𝐿1xydomFFyxzdomFdomGGz𝐿1
86 53 54 iblpos FMblFnG𝐿1xydomFFyxzdomFdomGGz𝐿1zdomFdomGGzMblFn2zifzdomFdomGGz0
87 85 86 mpbid FMblFnG𝐿1xydomFFyxzdomFdomGGzMblFn2zifzdomFdomGGz0
88 87 simprd FMblFnG𝐿1xydomFFyx2zifzdomFdomGGz0
89 88 adantr FMblFnG𝐿1xydomFFyx¬domFdomG=2zifzdomFdomGGz0
90 simplrl FMblFnG𝐿1xydomFFyx¬domFdomG=x
91 neq0 ¬domFdomG=zzdomFdomG
92 0re 0
93 92 a1i FMblFnG𝐿1xydomFFyxzdomFdomG0
94 elinel1 zdomFdomGzdomF
95 ffvelrn F:domFzdomFFz
96 2 94 95 syl2an FMblFnG𝐿1xydomFFyxzdomFdomGFz
97 96 abscld FMblFnG𝐿1xydomFFyxzdomFdomGFz
98 simplrl FMblFnG𝐿1xydomFFyxzdomFdomGx
99 96 absge0d FMblFnG𝐿1xydomFFyxzdomFdomG0Fz
100 simprr FMblFnG𝐿1xydomFFyxydomFFyx
101 2fveq3 y=zFy=Fz
102 101 breq1d y=zFyxFzx
103 102 rspccva ydomFFyxzdomFFzx
104 100 94 103 syl2an FMblFnG𝐿1xydomFFyxzdomFdomGFzx
105 93 97 98 99 104 letrd FMblFnG𝐿1xydomFFyxzdomFdomG0x
106 105 ex FMblFnG𝐿1xydomFFyxzdomFdomG0x
107 106 exlimdv FMblFnG𝐿1xydomFFyxzzdomFdomG0x
108 91 107 syl5bi FMblFnG𝐿1xydomFFyx¬domFdomG=0x
109 108 imp FMblFnG𝐿1xydomFFyx¬domFdomG=0x
110 elrege0 x0+∞x0x
111 90 109 110 sylanbrc FMblFnG𝐿1xydomFFyx¬domFdomG=x0+∞
112 76 89 111 itg2mulc FMblFnG𝐿1xydomFFyx¬domFdomG=2×x×fzifzdomFdomGGz0=x2zifzdomFdomGGz0
113 73 112 eqtr3d FMblFnG𝐿1xydomFFyx¬domFdomG=2zifzdomFdomGxGz0=x2zifzdomFdomGGz0
114 90 89 remulcld FMblFnG𝐿1xydomFFyx¬domFdomG=x2zifzdomFdomGGz0
115 113 114 eqeltrd FMblFnG𝐿1xydomFFyx¬domFdomG=2zifzdomFdomGxGz0
116 115 ex FMblFnG𝐿1xydomFFyx¬domFdomG=2zifzdomFdomGxGz0
117 noel ¬z
118 eleq2 domFdomG=zdomFdomGz
119 117 118 mtbiri domFdomG=¬zdomFdomG
120 iffalse ¬zdomFdomGifzdomFdomGxGz0=0
121 119 120 syl domFdomG=ifzdomFdomGxGz0=0
122 121 mpteq2dv domFdomG=zifzdomFdomGxGz0=z0
123 fconstmpt ×0=z0
124 122 123 eqtr4di domFdomG=zifzdomFdomGxGz0=×0
125 124 fveq2d domFdomG=2zifzdomFdomGxGz0=2×0
126 itg20 2×0=0
127 126 92 eqeltri 2×0
128 125 127 eqeltrdi domFdomG=2zifzdomFdomGxGz0
129 116 128 pm2.61d2 FMblFnG𝐿1xydomFFyx2zifzdomFdomGxGz0
130 98 53 remulcld FMblFnG𝐿1xydomFFyxzdomFdomGxGz
131 130 rexrd FMblFnG𝐿1xydomFFyxzdomFdomGxGz*
132 98 53 105 54 mulge0d FMblFnG𝐿1xydomFFyxzdomFdomG0xGz
133 elxrge0 xGz0+∞xGz*0xGz
134 131 132 133 sylanbrc FMblFnG𝐿1xydomFFyxzdomFdomGxGz0+∞
135 134 42 ifclda FMblFnG𝐿1xydomFFyxifzdomFdomGxGz00+∞
136 135 adantr FMblFnG𝐿1xydomFFyxzifzdomFdomGxGz00+∞
137 136 fmpttd FMblFnG𝐿1xydomFFyxzifzdomFdomGxGz0:0+∞
138 96 52 absmuld FMblFnG𝐿1xydomFFyxzdomFdomGFzGz=FzGz
139 abscl GzGz
140 absge0 Gz0Gz
141 139 140 jca GzGz0Gz
142 52 141 syl FMblFnG𝐿1xydomFFyxzdomFdomGGz0Gz
143 lemul1a FzxGz0GzFzxFzGzxGz
144 97 98 142 104 143 syl31anc FMblFnG𝐿1xydomFFyxzdomFdomGFzGzxGz
145 138 144 eqbrtrd FMblFnG𝐿1xydomFFyxzdomFdomGFzGzxGz
146 iftrue zdomFdomGifzdomFdomGFzGz0=FzGz
147 146 adantl FMblFnG𝐿1xydomFFyxzdomFdomGifzdomFdomGFzGz0=FzGz
148 iftrue zdomFdomGifzdomFdomGxGz0=xGz
149 148 adantl FMblFnG𝐿1xydomFFyxzdomFdomGifzdomFdomGxGz0=xGz
150 145 147 149 3brtr4d FMblFnG𝐿1xydomFFyxzdomFdomGifzdomFdomGFzGz0ifzdomFdomGxGz0
151 0le0 00
152 151 a1i ¬zdomFdomG00
153 iffalse ¬zdomFdomGifzdomFdomGFzGz0=0
154 152 153 120 3brtr4d ¬zdomFdomGifzdomFdomGFzGz0ifzdomFdomGxGz0
155 154 adantl FMblFnG𝐿1xydomFFyx¬zdomFdomGifzdomFdomGFzGz0ifzdomFdomGxGz0
156 150 155 pm2.61dan FMblFnG𝐿1xydomFFyxifzdomFdomGFzGz0ifzdomFdomGxGz0
157 156 ralrimivw FMblFnG𝐿1xydomFFyxzifzdomFdomGFzGz0ifzdomFdomGxGz0
158 46 a1i FMblFnG𝐿1xydomFFyxV
159 eqidd FMblFnG𝐿1xydomFFyxzifzdomFdomGFzGz0=zifzdomFdomGFzGz0
160 eqidd FMblFnG𝐿1xydomFFyxzifzdomFdomGxGz0=zifzdomFdomGxGz0
161 158 44 136 159 160 ofrfval2 FMblFnG𝐿1xydomFFyxzifzdomFdomGFzGz0fzifzdomFdomGxGz0zifzdomFdomGFzGz0ifzdomFdomGxGz0
162 157 161 mpbird FMblFnG𝐿1xydomFFyxzifzdomFdomGFzGz0fzifzdomFdomGxGz0
163 itg2le zifzdomFdomGFzGz0:0+∞zifzdomFdomGxGz0:0+∞zifzdomFdomGFzGz0fzifzdomFdomGxGz02zifzdomFdomGFzGz02zifzdomFdomGxGz0
164 45 137 162 163 syl3anc FMblFnG𝐿1xydomFFyx2zifzdomFdomGFzGz02zifzdomFdomGxGz0
165 itg2lecl zifzdomFdomGFzGz0:0+∞2zifzdomFdomGxGz02zifzdomFdomGFzGz02zifzdomFdomGxGz02zifzdomFdomGFzGz0
166 45 129 164 165 syl3anc FMblFnG𝐿1xydomFFyx2zifzdomFdomGFzGz0
167 36 38 iblpos FMblFnG𝐿1xydomFFyxzdomFdomGFzGz𝐿1zdomFdomGFzGzMblFn2zifzdomFdomGFzGz0
168 35 166 167 mpbir2and FMblFnG𝐿1xydomFFyxzdomFdomGFzGz𝐿1
169 17 20 168 iblabsr FMblFnG𝐿1xydomFFyxzdomFdomGFzGz𝐿1
170 16 169 eqeltrd FMblFnG𝐿1xydomFFyxF×fG𝐿1
171 170 rexlimdvaa FMblFnG𝐿1xydomFFyxF×fG𝐿1
172 171 3impia FMblFnG𝐿1xydomFFyxF×fG𝐿1