Metamath Proof Explorer


Theorem ditgswap

Description: Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses ditgcl.x
|- ( ph -> X e. RR )
ditgcl.y
|- ( ph -> Y e. RR )
ditgcl.a
|- ( ph -> A e. ( X [,] Y ) )
ditgcl.b
|- ( ph -> B e. ( X [,] Y ) )
ditgcl.c
|- ( ( ph /\ x e. ( X (,) Y ) ) -> C e. V )
ditgcl.i
|- ( ph -> ( x e. ( X (,) Y ) |-> C ) e. L^1 )
Assertion ditgswap
|- ( ph -> S_ [ B -> A ] C _d x = -u S_ [ A -> B ] C _d x )

Proof

Step Hyp Ref Expression
1 ditgcl.x
 |-  ( ph -> X e. RR )
2 ditgcl.y
 |-  ( ph -> Y e. RR )
3 ditgcl.a
 |-  ( ph -> A e. ( X [,] Y ) )
4 ditgcl.b
 |-  ( ph -> B e. ( X [,] Y ) )
5 ditgcl.c
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> C e. V )
6 ditgcl.i
 |-  ( ph -> ( x e. ( X (,) Y ) |-> C ) e. L^1 )
7 elicc2
 |-  ( ( X e. RR /\ Y e. RR ) -> ( A e. ( X [,] Y ) <-> ( A e. RR /\ X <_ A /\ A <_ Y ) ) )
8 1 2 7 syl2anc
 |-  ( ph -> ( A e. ( X [,] Y ) <-> ( A e. RR /\ X <_ A /\ A <_ Y ) ) )
9 3 8 mpbid
 |-  ( ph -> ( A e. RR /\ X <_ A /\ A <_ Y ) )
10 9 simp1d
 |-  ( ph -> A e. RR )
11 elicc2
 |-  ( ( X e. RR /\ Y e. RR ) -> ( B e. ( X [,] Y ) <-> ( B e. RR /\ X <_ B /\ B <_ Y ) ) )
12 1 2 11 syl2anc
 |-  ( ph -> ( B e. ( X [,] Y ) <-> ( B e. RR /\ X <_ B /\ B <_ Y ) ) )
13 4 12 mpbid
 |-  ( ph -> ( B e. RR /\ X <_ B /\ B <_ Y ) )
14 13 simp1d
 |-  ( ph -> B e. RR )
15 simpr
 |-  ( ( ph /\ A <_ B ) -> A <_ B )
16 10 adantr
 |-  ( ( ph /\ A <_ B ) -> A e. RR )
17 14 adantr
 |-  ( ( ph /\ A <_ B ) -> B e. RR )
18 15 16 17 ditgneg
 |-  ( ( ph /\ A <_ B ) -> S_ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x )
19 15 ditgpos
 |-  ( ( ph /\ A <_ B ) -> S_ [ A -> B ] C _d x = S. ( A (,) B ) C _d x )
20 19 negeqd
 |-  ( ( ph /\ A <_ B ) -> -u S_ [ A -> B ] C _d x = -u S. ( A (,) B ) C _d x )
21 18 20 eqtr4d
 |-  ( ( ph /\ A <_ B ) -> S_ [ B -> A ] C _d x = -u S_ [ A -> B ] C _d x )
22 1 rexrd
 |-  ( ph -> X e. RR* )
23 13 simp2d
 |-  ( ph -> X <_ B )
24 iooss1
 |-  ( ( X e. RR* /\ X <_ B ) -> ( B (,) A ) C_ ( X (,) A ) )
25 22 23 24 syl2anc
 |-  ( ph -> ( B (,) A ) C_ ( X (,) A ) )
26 2 rexrd
 |-  ( ph -> Y e. RR* )
27 9 simp3d
 |-  ( ph -> A <_ Y )
28 iooss2
 |-  ( ( Y e. RR* /\ A <_ Y ) -> ( X (,) A ) C_ ( X (,) Y ) )
29 26 27 28 syl2anc
 |-  ( ph -> ( X (,) A ) C_ ( X (,) Y ) )
30 25 29 sstrd
 |-  ( ph -> ( B (,) A ) C_ ( X (,) Y ) )
31 30 sselda
 |-  ( ( ph /\ x e. ( B (,) A ) ) -> x e. ( X (,) Y ) )
32 iblmbf
 |-  ( ( x e. ( X (,) Y ) |-> C ) e. L^1 -> ( x e. ( X (,) Y ) |-> C ) e. MblFn )
33 6 32 syl
 |-  ( ph -> ( x e. ( X (,) Y ) |-> C ) e. MblFn )
34 33 5 mbfmptcl
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> C e. CC )
35 31 34 syldan
 |-  ( ( ph /\ x e. ( B (,) A ) ) -> C e. CC )
36 ioombl
 |-  ( B (,) A ) e. dom vol
37 36 a1i
 |-  ( ph -> ( B (,) A ) e. dom vol )
38 30 37 5 6 iblss
 |-  ( ph -> ( x e. ( B (,) A ) |-> C ) e. L^1 )
39 35 38 itgcl
 |-  ( ph -> S. ( B (,) A ) C _d x e. CC )
40 39 adantr
 |-  ( ( ph /\ B <_ A ) -> S. ( B (,) A ) C _d x e. CC )
41 40 negnegd
 |-  ( ( ph /\ B <_ A ) -> -u -u S. ( B (,) A ) C _d x = S. ( B (,) A ) C _d x )
42 simpr
 |-  ( ( ph /\ B <_ A ) -> B <_ A )
43 14 adantr
 |-  ( ( ph /\ B <_ A ) -> B e. RR )
44 10 adantr
 |-  ( ( ph /\ B <_ A ) -> A e. RR )
45 42 43 44 ditgneg
 |-  ( ( ph /\ B <_ A ) -> S_ [ A -> B ] C _d x = -u S. ( B (,) A ) C _d x )
46 45 negeqd
 |-  ( ( ph /\ B <_ A ) -> -u S_ [ A -> B ] C _d x = -u -u S. ( B (,) A ) C _d x )
47 42 ditgpos
 |-  ( ( ph /\ B <_ A ) -> S_ [ B -> A ] C _d x = S. ( B (,) A ) C _d x )
48 41 46 47 3eqtr4rd
 |-  ( ( ph /\ B <_ A ) -> S_ [ B -> A ] C _d x = -u S_ [ A -> B ] C _d x )
49 10 14 21 48 lecasei
 |-  ( ph -> S_ [ B -> A ] C _d x = -u S_ [ A -> B ] C _d x )