This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ditgcl

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

Ref Expression
Hypotheses ditgcl.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
ditgcl.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
ditgcl.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
ditgcl.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
ditgcl.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ 𝑉 )
ditgcl.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ 𝐿1 )
Assertion ditgcl ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 ∈ ℂ )

Proof

Step Hyp Ref Expression
1 ditgcl.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 ditgcl.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 ditgcl.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
4 ditgcl.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
5 ditgcl.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ 𝑉 )
6 ditgcl.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ 𝐿1 )
7 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
9 3 8 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) )
10 9 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
13 4 12 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) )
14 13 simp1d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
15 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
16 15 ditgpos ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
17 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
18 9 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐴 )
19 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
20 17 18 19 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
21 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
22 13 simp3d ⊢ ( 𝜑 → 𝐵 ≤ 𝑌 )
23 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐵 ≤ 𝑌 ) → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
24 21 22 23 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
25 20 24 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
26 25 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
27 26 5 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ 𝑉 )
28 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
29 28 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
30 25 29 5 6 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 )
31 27 30 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 ∈ ℂ )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 ∈ ℂ )
33 16 32 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 ∈ ℂ )
34 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 )
35 14 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ∈ ℝ )
36 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
37 34 35 36 ditgneg ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
38 13 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
39 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐵 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝐴 ) )
40 17 38 39 syl2anc ⊢ ( 𝜑 → ( 𝐵 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝐴 ) )
41 9 simp3d ⊢ ( 𝜑 → 𝐴 ≤ 𝑌 )
42 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐴 ≤ 𝑌 ) → ( 𝑋 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝑌 ) )
43 21 41 42 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝑌 ) )
44 40 43 sstrd ⊢ ( 𝜑 → ( 𝐵 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝑌 ) )
45 44 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
46 45 5 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) ) → 𝐶 ∈ 𝑉 )
47 ioombl ⊢ ( 𝐵 (,) 𝐴 ) ∈ dom vol
48 47 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐴 ) ∈ dom vol )
49 44 48 5 6 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,) 𝐴 ) ↦ 𝐶 ) ∈ 𝐿1 )
50 46 49 itgcl ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ∈ ℂ )
51 50 negcld ⊢ ( 𝜑 → - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ∈ ℂ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ∈ ℂ )
53 37 52 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 ∈ ℂ )
54 10 14 33 53 lecasei ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 ∈ ℂ )