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

Metamath Proof Explorer

Theorem itgsub

Description: Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion itgsub ( 𝜑 → ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6 2 5 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7 6 1 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
9 4 8 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
10 9 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
11 10 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
12 3 4 iblneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ 𝐿1 )
13 7 2 11 12 itgadd ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 - 𝐶 d 𝑥 ) )
14 3 4 itgneg ⊢ ( 𝜑 → - ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐴 - 𝐶 d 𝑥 )
15 14 oveq2d ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 - 𝐶 d 𝑥 ) )
16 13 15 eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) )
17 7 10 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
18 17 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 )
19 1 2 itgcl ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
20 3 4 itgcl ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 ∈ ℂ )
21 19 20 negsubd ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )
22 16 18 21 3eqtr3d ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )