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 
|- ( ( ph /\ x e. A ) -> B e. V )
itgadd.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgadd.3 
|- ( ( ph /\ x e. A ) -> C e. V )
itgadd.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
Assertion itgsub 
|- ( ph -> S. A ( B - C ) _d x = ( S. A B _d x - S. A C _d x ) )

Proof

Step Hyp Ref Expression
1 itgadd.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgadd.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 itgadd.3 
 |-  ( ( ph /\ x e. A ) -> C e. V )
4 itgadd.4 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
5 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
6 2 5 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
7 6 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
8 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
9 4 8 syl 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
10 9 3 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
11 10 negcld 
 |-  ( ( ph /\ x e. A ) -> -u C e. CC )
12 3 4 iblneg 
 |-  ( ph -> ( x e. A |-> -u C ) e. L^1 )
13 7 2 11 12 itgadd 
 |-  ( ph -> S. A ( B + -u C ) _d x = ( S. A B _d x + S. A -u C _d x ) )
14 3 4 itgneg 
 |-  ( ph -> -u S. A C _d x = S. A -u C _d x )
15 14 oveq2d 
 |-  ( ph -> ( S. A B _d x + -u S. A C _d x ) = ( S. A B _d x + S. A -u C _d x ) )
16 13 15 eqtr4d 
 |-  ( ph -> S. A ( B + -u C ) _d x = ( S. A B _d x + -u S. A C _d x ) )
17 7 10 negsubd 
 |-  ( ( ph /\ x e. A ) -> ( B + -u C ) = ( B - C ) )
18 17 itgeq2dv 
 |-  ( ph -> S. A ( B + -u C ) _d x = S. A ( B - C ) _d x )
19 1 2 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
20 3 4 itgcl 
 |-  ( ph -> S. A C _d x e. CC )
21 19 20 negsubd 
 |-  ( ph -> ( S. A B _d x + -u S. A C _d x ) = ( S. A B _d x - S. A C _d x ) )
22 16 18 21 3eqtr3d 
 |-  ( ph -> S. A ( B - C ) _d x = ( S. A B _d x - S. A C _d x ) )