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 𝑥 ∈ ℂ )