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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	itgvol0.2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
	itgvol0.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	itgvol0	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ∧ ∫ 𝐴 𝐵 d 𝑥 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		itgvol0.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		itgvol0.2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
3		itgvol0.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ 𝐵 ) = ∅
5		iblempty	⊢ ∅ ∈ 𝐿1
6	4 5	eqeltri	⊢ ( 𝑥 ∈ ∅ ↦ 𝐵 ) ∈ 𝐿1
7		0ss	⊢ ∅ ⊆ 𝐴
8	7	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝐴 )
9		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ ∅ ) ⊆ 𝐴 )
10		ovolssnul	⊢ ( ( ( 𝐴 ∖ ∅ ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ( vol* ‘ ( 𝐴 ∖ ∅ ) ) = 0 )
11	9 1 2 10	syl3anc	⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∖ ∅ ) ) = 0 )
12	8 1 11 3	itgss3	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ∅ ↦ 𝐵 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ) ∧ ∫ ∅ 𝐵 d 𝑥 = ∫ 𝐴 𝐵 d 𝑥 ) )
13	12	simpld	⊢ ( 𝜑 → ( ( 𝑥 ∈ ∅ ↦ 𝐵 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ) )
14	6 13	mpbii	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
15		itg0	⊢ ∫ ∅ 𝐵 d 𝑥 = 0
16	12	simprd	⊢ ( 𝜑 → ∫ ∅ 𝐵 d 𝑥 = ∫ 𝐴 𝐵 d 𝑥 )
17	15 16	syl5reqr	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = 0 )
18	14 17	jca	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ∧ ∫ 𝐴 𝐵 d 𝑥 = 0 ) )