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 ⊢φ→∫AB−Cdx=∫ABdx−∫ACdx

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 ⊢φ→∫AB+−Cdx=∫ABdx+∫A−Cdx
18 3 4 itgneg ⊢φ→−∫ACdx=∫A−Cdx
19 18 oveq2d ⊢φ→∫ABdx+−∫ACdx=∫ABdx+∫A−Cdx
20 17 19 eqtr4d ⊢φ→∫AB+−Cdx=∫ABdx+−∫ACdx
21 14 itgeq2dv ⊢φ→∫AB+−Cdx=∫AB−Cdx
22 1 2 itgcl ⊢φ→∫ABdx∈ℂ
23 3 4 itgcl ⊢φ→∫ACdx∈ℂ
24 22 23 negsubd ⊢φ→∫ABdx+−∫ACdx=∫ABdx−∫ACdx
25 20 21 24 3eqtr3d ⊢φ→∫AB−Cdx=∫ABdx−∫ACdx