Metamath Proof Explorer

Theorem itgsubnc

Description: Choice-free analogue of itgsub . (Contributed by Brendan Leahy, 11-Nov-2017)

Ref Expression
Hypotheses ibladdnc.1 ⊢ φ ∧ x ∈ A → B ∈ V
ibladdnc.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
ibladdnc.3 ⊢ φ ∧ x ∈ A → C ∈ V
ibladdnc.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
iblsubnc.m ⊢ φ → x ∈ A ⟼ B − C ∈ MblFn
Assertion itgsubnc ⊢ φ → ∫ A B − C dx = ∫ A B dx − ∫ A C dx

Proof

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