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 )