Metamath Proof Explorer

Theorem itgsubnc

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

Ref Expression
Hypotheses ibladdnc.1 
|- ( ( ph /\ x e. A ) -> B e. V )
ibladdnc.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
ibladdnc.3 
|- ( ( ph /\ x e. A ) -> C e. V )
ibladdnc.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
iblsubnc.m 
|- ( ph -> ( x e. A |-> ( B - C ) ) e. MblFn )
Assertion itgsubnc 
|- ( ph -> S. A ( B - C ) _d x = ( S. A B _d x - S. A C _d x ) )

Proof

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