This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
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 12 simprd ⊢ ( 𝜑 → ∫ ∅ 𝐵 d 𝑥 = ∫ 𝐴 𝐵 d 𝑥 )
16 itg0 ⊢ ∫ ∅ 𝐵 d 𝑥 = 0
17 15 16 eqtr3di ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = 0 )
18 14 17 jca ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ∧ ∫ 𝐴 𝐵 d 𝑥 = 0 ) )