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	|- ( ph -> A C_ RR )
	itgvol0.2	|- ( ph -> ( vol* ` A ) = 0 )
	itgvol0.3	|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion	itgvol0	|- ( ph -> ( ( x e. A |-> B ) e. L^1 /\ S. A B _d x = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		itgvol0.1	|- ( ph -> A C_ RR )
2		itgvol0.2	|- ( ph -> ( vol* ` A ) = 0 )
3		itgvol0.3	|- ( ( ph /\ x e. A ) -> B e. CC )
4		mpt0	|- ( x e. (/) |-> B ) = (/)
5		iblempty	|- (/) e. L^1
6	4 5	eqeltri	|- ( x e. (/) |-> B ) e. L^1
7		0ss	|- (/) C_ A
8	7	a1i	|- ( ph -> (/) C_ A )
9		difssd	|- ( ph -> ( A \ (/) ) C_ A )
10		ovolssnul	|- ( ( ( A \ (/) ) C_ A /\ A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( A \ (/) ) ) = 0 )
11	9 1 2 10	syl3anc	|- ( ph -> ( vol* ` ( A \ (/) ) ) = 0 )
12	8 1 11 3	itgss3	|- ( ph -> ( ( ( x e. (/) |-> B ) e. L^1 <-> ( x e. A |-> B ) e. L^1 ) /\ S. (/) B _d x = S. A B _d x ) )
13	12	simpld	|- ( ph -> ( ( x e. (/) |-> B ) e. L^1 <-> ( x e. A |-> B ) e. L^1 ) )
14	6 13	mpbii	|- ( ph -> ( x e. A |-> B ) e. L^1 )
15		itg0	|- S. (/) B _d x = 0
16	12	simprd	|- ( ph -> S. (/) B _d x = S. A B _d x )
17	15 16	syl5reqr	|- ( ph -> S. A B _d x = 0 )
18	14 17	jca	|- ( ph -> ( ( x e. A |-> B ) e. L^1 /\ S. A B _d x = 0 ) )