Theorem ftc2ditg

Description: Directed integral analogue of ftc2 . (Contributed by Mario Carneiro, 3-Sep-2014)

	Ref	Expression
Hypotheses	ftc2ditg.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	ftc2ditg.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	ftc2ditg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
	ftc2ditg.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
	ftc2ditg.c	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
	ftc2ditg.i	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿1 )
	ftc2ditg.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
Assertion	ftc2ditg	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ftc2ditg.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2		ftc2ditg.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3		ftc2ditg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
4		ftc2ditg.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
5		ftc2ditg.c	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
6		ftc2ditg.i	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿1 )
7		ftc2ditg.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
8		iccssre	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
10	9 3	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11	9 4	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12	1 2 3 4 5 6 7	ftc2ditglem	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
13		fvexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
14		cncff	⊢ ( ( ℝ D 𝐹 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( ℝ D 𝐹 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
15	5 14	syl	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
16	15	feqmptd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
17	16 6	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿1 )
18	1 2 4 3 13 17	ditgswap	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = - ⨜ [ 𝐵 → 𝐴 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = - ⨜ [ 𝐵 → 𝐴 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
20	1 2 4 3 5 6 7	ftc2ditglem	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐵 → 𝐴 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) )
21	20	negeqd	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → - ⨜ [ 𝐵 → 𝐴 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = - ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) )
22		cncff	⊢ ( 𝐹 ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → 𝐹 : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
23	7 22	syl	⊢ ( 𝜑 → 𝐹 : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
24	23 3	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
25	23 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
26	24 25	negsubdi2d	⊢ ( 𝜑 → - ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → - ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
28	19 21 27	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
29	10 11 12 28	lecasei	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )