Metamath Proof Explorer


Theorem ibl0

Description: The zero function is integrable on any measurable set. (Unlike iblconst , this does not require A to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion ibl0 A dom vol A × 0 𝐿 1

Proof

Step Hyp Ref Expression
1 0cn 0
2 mbfconst A dom vol 0 A × 0 MblFn
3 1 2 mpan2 A dom vol A × 0 MblFn
4 ax-icn i
5 ine0 i 0
6 elfzelz k 0 3 k
7 6 ad2antlr A dom vol k 0 3 x A k
8 expclz i i 0 k i k
9 expne0i i i 0 k i k 0
10 8 9 div0d i i 0 k 0 i k = 0
11 4 5 7 10 mp3an12i A dom vol k 0 3 x A 0 i k = 0
12 11 fveq2d A dom vol k 0 3 x A 0 i k = 0
13 re0 0 = 0
14 12 13 syl6eq A dom vol k 0 3 x A 0 i k = 0
15 14 itgvallem3 A dom vol k 0 3 2 x if x A 0 0 i k 0 i k 0 = 0
16 0re 0
17 15 16 syl6eqel A dom vol k 0 3 2 x if x A 0 0 i k 0 i k 0
18 17 ralrimiva A dom vol k 0 3 2 x if x A 0 0 i k 0 i k 0
19 eqidd A dom vol x if x A 0 0 i k 0 i k 0 = x if x A 0 0 i k 0 i k 0
20 eqidd A dom vol x A 0 i k = 0 i k
21 c0ex 0 V
22 21 fconst A × 0 : A 0
23 fdm A × 0 : A 0 dom A × 0 = A
24 22 23 mp1i A dom vol dom A × 0 = A
25 21 fvconst2 x A A × 0 x = 0
26 25 adantl A dom vol x A A × 0 x = 0
27 19 20 24 26 isibl A dom vol A × 0 𝐿 1 A × 0 MblFn k 0 3 2 x if x A 0 0 i k 0 i k 0
28 3 18 27 mpbir2and A dom vol A × 0 𝐿 1