Metamath Proof Explorer

Theorem ftc2ditg

Description: Directed integral analogue of ftc2 . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses ftc2ditg.x 
|- ( ph -> X e. RR )
ftc2ditg.y 
|- ( ph -> Y e. RR )
ftc2ditg.a 
|- ( ph -> A e. ( X [,] Y ) )
ftc2ditg.b 
|- ( ph -> B e. ( X [,] Y ) )
ftc2ditg.c 
|- ( ph -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )
ftc2ditg.i 
|- ( ph -> ( RR _D F ) e. L^1 )
ftc2ditg.f 
|- ( ph -> F e. ( ( X [,] Y ) -cn-> CC ) )
Assertion ftc2ditg 
|- ( ph -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 ftc2ditg.x 
 |-  ( ph -> X e. RR )
2 ftc2ditg.y 
 |-  ( ph -> Y e. RR )
3 ftc2ditg.a 
 |-  ( ph -> A e. ( X [,] Y ) )
4 ftc2ditg.b 
 |-  ( ph -> B e. ( X [,] Y ) )
5 ftc2ditg.c 
 |-  ( ph -> ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) )
6 ftc2ditg.i 
 |-  ( ph -> ( RR _D F ) e. L^1 )
7 ftc2ditg.f 
 |-  ( ph -> F e. ( ( X [,] Y ) -cn-> CC ) )
8 iccssre 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( X [,] Y ) C_ RR )
9 1 2 8 syl2anc 
 |-  ( ph -> ( X [,] Y ) C_ RR )
10 9 3 sseldd 
 |-  ( ph -> A e. RR )
11 9 4 sseldd 
 |-  ( ph -> B e. RR )
12 1 2 3 4 5 6 7 ftc2ditglem 
 |-  ( ( ph /\ A <_ B ) -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
13 fvexd 
 |-  ( ( ph /\ t e. ( X (,) Y ) ) -> ( ( RR _D F ) ` t ) e. _V )
14 cncff 
 |-  ( ( RR _D F ) e. ( ( X (,) Y ) -cn-> CC ) -> ( RR _D F ) : ( X (,) Y ) --> CC )
15 5 14 syl 
 |-  ( ph -> ( RR _D F ) : ( X (,) Y ) --> CC )
16 15 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) )
17 16 6 eqeltrrd 
 |-  ( ph -> ( t e. ( X (,) Y ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
18 1 2 4 3 13 17 ditgswap 
 |-  ( ph -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = -u S_ [ B -> A ] ( ( RR _D F ) ` t ) _d t )
19 18 adantr 
 |-  ( ( ph /\ B <_ A ) -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = -u S_ [ B -> A ] ( ( RR _D F ) ` t ) _d t )
20 1 2 4 3 5 6 7 ftc2ditglem 
 |-  ( ( ph /\ B <_ A ) -> S_ [ B -> A ] ( ( RR _D F ) ` t ) _d t = ( ( F ` A ) - ( F ` B ) ) )
21 20 negeqd 
 |-  ( ( ph /\ B <_ A ) -> -u S_ [ B -> A ] ( ( RR _D F ) ` t ) _d t = -u ( ( F ` A ) - ( F ` B ) ) )
22 cncff 
 |-  ( F e. ( ( X [,] Y ) -cn-> CC ) -> F : ( X [,] Y ) --> CC )
23 7 22 syl 
 |-  ( ph -> F : ( X [,] Y ) --> CC )
24 23 3 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. CC )
25 23 4 ffvelrnd 
 |-  ( ph -> ( F ` B ) e. CC )
26 24 25 negsubdi2d 
 |-  ( ph -> -u ( ( F ` A ) - ( F ` B ) ) = ( ( F ` B ) - ( F ` A ) ) )
27 26 adantr 
 |-  ( ( ph /\ B <_ A ) -> -u ( ( F ` A ) - ( F ` B ) ) = ( ( F ` B ) - ( F ` A ) ) )
28 19 21 27 3eqtrd 
 |-  ( ( ph /\ B <_ A ) -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )
29 10 11 12 28 lecasei 
 |-  ( ph -> S_ [ A -> B ] ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )