This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 iblsub 
|- ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )

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 7 10 negsubd 
 |-  ( ( ph /\ x e. A ) -> ( B + -u C ) = ( B - C ) )
12 11 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( B + -u C ) ) = ( x e. A |-> ( B - C ) ) )
13 10 negcld 
 |-  ( ( ph /\ x e. A ) -> -u C e. CC )
14 3 4 iblneg 
 |-  ( ph -> ( x e. A |-> -u C ) e. L^1 )
15 7 2 13 14 ibladd 
 |-  ( ph -> ( x e. A |-> ( B + -u C ) ) e. L^1 )
16 12 15 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )