# 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 ${⊢}{\phi }\to {A}\subseteq ℝ$
itgvol0.2 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=0$
itgvol0.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
Assertion itgvol0 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\wedge {\int }_{{A}}{B}d{x}=0\right)$

### Proof

Step Hyp Ref Expression
1 itgvol0.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 itgvol0.2 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)=0$
3 itgvol0.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
4 mpt0 ${⊢}\left({x}\in \varnothing ⟼{B}\right)=\varnothing$
5 iblempty ${⊢}\varnothing \in {𝐿}^{1}$
6 4 5 eqeltri ${⊢}\left({x}\in \varnothing ⟼{B}\right)\in {𝐿}^{1}$
7 0ss ${⊢}\varnothing \subseteq {A}$
8 7 a1i ${⊢}{\phi }\to \varnothing \subseteq {A}$
9 difssd ${⊢}{\phi }\to {A}\setminus \varnothing \subseteq {A}$
10 ovolssnul ${⊢}\left({A}\setminus \varnothing \subseteq {A}\wedge {A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)=0\right)\to {vol}^{*}\left({A}\setminus \varnothing \right)=0$
11 9 1 2 10 syl3anc ${⊢}{\phi }\to {vol}^{*}\left({A}\setminus \varnothing \right)=0$
12 8 1 11 3 itgss3 ${⊢}{\phi }\to \left(\left(\left({x}\in \varnothing ⟼{B}\right)\in {𝐿}^{1}↔\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\right)\wedge {\int }_{\varnothing }{B}d{x}={\int }_{{A}}{B}d{x}\right)$
13 12 simpld ${⊢}{\phi }\to \left(\left({x}\in \varnothing ⟼{B}\right)\in {𝐿}^{1}↔\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\right)$
14 6 13 mpbii ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
15 itg0 ${⊢}{\int }_{\varnothing }{B}d{x}=0$
16 12 simprd ${⊢}{\phi }\to {\int }_{\varnothing }{B}d{x}={\int }_{{A}}{B}d{x}$
17 15 16 syl5reqr ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}=0$
18 14 17 jca ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\wedge {\int }_{{A}}{B}d{x}=0\right)$