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

Metamath Proof Explorer

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 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )