Metamath Proof Explorer

Theorem iblsub

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 iblsub ⊢ φ → x ∈ A ⟼ B − C ∈ 𝐿 1

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 7 10 negsubd ⊢ φ ∧ x ∈ A → B + − C = B − C
12 11 mpteq2dva ⊢ φ → x ∈ A ⟼ B + − C = x ∈ A ⟼ B − C
13 10 negcld ⊢ φ ∧ x ∈ A → − C ∈ ℂ
14 3 4 iblneg ⊢ φ → x ∈ A ⟼ − C ∈ 𝐿 1
15 7 2 13 14 ibladd ⊢ φ → x ∈ A ⟼ B + − C ∈ 𝐿 1
16 12 15 eqeltrrd ⊢ φ → x ∈ A ⟼ B − C ∈ 𝐿 1