Metamath Proof Explorer


Theorem itgvol0

Description: If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgvol0.1 φ A
itgvol0.2 φ vol * A = 0
itgvol0.3 φ x A B
Assertion itgvol0 φ x A B 𝐿 1 A B dx = 0

Proof

Step Hyp Ref Expression
1 itgvol0.1 φ A
2 itgvol0.2 φ vol * A = 0
3 itgvol0.3 φ x A B
4 mpt0 x B =
5 iblempty 𝐿 1
6 4 5 eqeltri x B 𝐿 1
7 0ss A
8 7 a1i φ A
9 difssd φ A A
10 ovolssnul A A A vol * A = 0 vol * A = 0
11 9 1 2 10 syl3anc φ vol * A = 0
12 8 1 11 3 itgss3 φ x B 𝐿 1 x A B 𝐿 1 B dx = A B dx
13 12 simpld φ x B 𝐿 1 x A B 𝐿 1
14 6 13 mpbii φ x A B 𝐿 1
15 12 simprd φ B dx = A B dx
16 itg0 B dx = 0
17 15 16 eqtr3di φ A B dx = 0
18 14 17 jca φ x A B 𝐿 1 A B dx = 0