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 𝑥 ) )