Metamath Proof Explorer

Theorem ditgcl

Description: Closure of 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 ditgcl 
|- ( ph -> S_ [ A -> B ] C _d x e. CC )

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 15 ditgpos 
 |-  ( ( ph /\ A <_ B ) -> S_ [ A -> B ] C _d x = S. ( A (,) B ) C _d x )
17 1 rexrd 
 |-  ( ph -> X e. RR* )
18 9 simp2d 
 |-  ( ph -> X <_ A )
19 iooss1 
 |-  ( ( X e. RR* /\ X <_ A ) -> ( A (,) B ) C_ ( X (,) B ) )
20 17 18 19 syl2anc 
 |-  ( ph -> ( A (,) B ) C_ ( X (,) B ) )
21 2 rexrd 
 |-  ( ph -> Y e. RR* )
22 13 simp3d 
 |-  ( ph -> B <_ Y )
23 iooss2 
 |-  ( ( Y e. RR* /\ B <_ Y ) -> ( X (,) B ) C_ ( X (,) Y ) )
24 21 22 23 syl2anc 
 |-  ( ph -> ( X (,) B ) C_ ( X (,) Y ) )
25 20 24 sstrd 
 |-  ( ph -> ( A (,) B ) C_ ( X (,) Y ) )
26 25 sselda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( X (,) Y ) )
27 26 5 syldan 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> C e. V )
28 ioombl 
 |-  ( A (,) B ) e. dom vol
29 28 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
30 25 29 5 6 iblss 
 |-  ( ph -> ( x e. ( A (,) B ) |-> C ) e. L^1 )
31 27 30 itgcl 
 |-  ( ph -> S. ( A (,) B ) C _d x e. CC )
32 31 adantr 
 |-  ( ( ph /\ A <_ B ) -> S. ( A (,) B ) C _d x e. CC )
33 16 32 eqeltrd 
 |-  ( ( ph /\ A <_ B ) -> S_ [ A -> B ] C _d x e. CC )
34 simpr 
 |-  ( ( ph /\ B <_ A ) -> B <_ A )
35 14 adantr 
 |-  ( ( ph /\ B <_ A ) -> B e. RR )
36 10 adantr 
 |-  ( ( ph /\ B <_ A ) -> A e. RR )
37 34 35 36 ditgneg 
 |-  ( ( ph /\ B <_ A ) -> S_ [ A -> B ] C _d x = -u S. ( B (,) A ) C _d x )
38 13 simp2d 
 |-  ( ph -> X <_ B )
39 iooss1 
 |-  ( ( X e. RR* /\ X <_ B ) -> ( B (,) A ) C_ ( X (,) A ) )
40 17 38 39 syl2anc 
 |-  ( ph -> ( B (,) A ) C_ ( X (,) A ) )
41 9 simp3d 
 |-  ( ph -> A <_ Y )
42 iooss2 
 |-  ( ( Y e. RR* /\ A <_ Y ) -> ( X (,) A ) C_ ( X (,) Y ) )
43 21 41 42 syl2anc 
 |-  ( ph -> ( X (,) A ) C_ ( X (,) Y ) )
44 40 43 sstrd 
 |-  ( ph -> ( B (,) A ) C_ ( X (,) Y ) )
45 44 sselda 
 |-  ( ( ph /\ x e. ( B (,) A ) ) -> x e. ( X (,) Y ) )
46 45 5 syldan 
 |-  ( ( ph /\ x e. ( B (,) A ) ) -> C e. V )
47 ioombl 
 |-  ( B (,) A ) e. dom vol
48 47 a1i 
 |-  ( ph -> ( B (,) A ) e. dom vol )
49 44 48 5 6 iblss 
 |-  ( ph -> ( x e. ( B (,) A ) |-> C ) e. L^1 )
50 46 49 itgcl 
 |-  ( ph -> S. ( B (,) A ) C _d x e. CC )
51 50 negcld 
 |-  ( ph -> -u S. ( B (,) A ) C _d x e. CC )
52 51 adantr 
 |-  ( ( ph /\ B <_ A ) -> -u S. ( B (,) A ) C _d x e. CC )
53 37 52 eqeltrd 
 |-  ( ( ph /\ B <_ A ) -> S_ [ A -> B ] C _d x e. CC )
54 10 14 33 53 lecasei 
 |-  ( ph -> S_ [ A -> B ] C _d x e. CC )