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 ⊢ φ ∧ x ∈ A → B ∈ V
itgadd.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgadd.3 ⊢ φ ∧ x ∈ A → C ∈ V
itgadd.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
Assertion itgsub ⊢ φ → ∫ A B − C dx = ∫ A B dx − ∫ A C dx

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 itgadd.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 itgadd.3 ⊢ φ ∧ x ∈ A → C ∈ V
4 itgadd.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
5 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
6 2 5 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
7 6 1 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
8 iblmbf ⊢ x ∈ A ⟼ C ∈ 𝐿 1 → x ∈ A ⟼ C ∈ MblFn
9 4 8 syl ⊢ φ → x ∈ A ⟼ C ∈ MblFn
10 9 3 mbfmptcl ⊢ φ ∧ x ∈ A → C ∈ ℂ
11 10 negcld ⊢ φ ∧ x ∈ A → − C ∈ ℂ
12 3 4 iblneg ⊢ φ → x ∈ A ⟼ − C ∈ 𝐿 1
13 7 2 11 12 itgadd ⊢ φ → ∫ A B + − C dx = ∫ A B dx + ∫ A − C dx
14 3 4 itgneg ⊢ φ → − ∫ A C dx = ∫ A − C dx
15 14 oveq2d ⊢ φ → ∫ A B dx + − ∫ A C dx = ∫ A B dx + ∫ A − C dx
16 13 15 eqtr4d ⊢ φ → ∫ A B + − C dx = ∫ A B dx + − ∫ A C dx
17 7 10 negsubd ⊢ φ ∧ x ∈ A → B + − C = B − C
18 17 itgeq2dv ⊢ φ → ∫ A B + − C dx = ∫ A B − C dx
19 1 2 itgcl ⊢ φ → ∫ A B dx ∈ ℂ
20 3 4 itgcl ⊢ φ → ∫ A C dx ∈ ℂ
21 19 20 negsubd ⊢ φ → ∫ A B dx + − ∫ A C dx = ∫ A B dx − ∫ A C dx
22 16 18 21 3eqtr3d ⊢ φ → ∫ A B − C dx = ∫ A B dx − ∫ A C dx