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 )