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}Bdx=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\leftrightarrow \left(x\in A⟼B\right)\in {𝐿}^1\right)\wedge {\int }_{\varnothing }Bdx={\int }_{A}Bdx\right)$$
13	12	simpld	$$⊢\phi \to \left(\left(x\in \varnothing ⟼B\right)\in {𝐿}^1\leftrightarrow \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 }Bdx=0$$
16	12	simprd	$$⊢\phi \to {\int }_{\varnothing }Bdx={\int }_{A}Bdx$$
17	15 16	syl5reqr	$$⊢\phi \to {\int }_{A}Bdx=0$$
18	14 17	jca	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\wedge {\int }_{A}Bdx=0\right)$$