Metamath Proof Explorer

Theorem ftc2ditglem

Description: Lemma for ftc2ditg . (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 ftc2ditglem ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ 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 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
9 8 ditgpos ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
10 iccssre ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
11 1 2 10 syl2anc ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
12 11 3 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
14 11 4 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
16 ax-resscn ⊢ ℝ ⊆ ℂ
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ℝ ⊆ ℂ )
18 cncff ⊢ ( 𝐹 ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → 𝐹 : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
19 7 18 syl ⊢ ( 𝜑 → 𝐹 : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐹 : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
21 11 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
22 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
23 12 14 22 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
25 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
26 25 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
27 25 26 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝑋 [,] 𝑌 ) ⟶ ℂ ) ∧ ( ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
28 17 20 21 24 27 syl22anc ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
29 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
30 12 14 29 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
32 31 reseq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) )
33 28 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) )
34 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
35 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
36 1 2 35 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
37 3 36 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) )
38 37 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐴 )
39 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
40 34 38 39 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
41 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
42 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
43 1 2 42 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
44 4 43 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) )
45 44 simp3d ⊢ ( 𝜑 → 𝐵 ≤ 𝑌 )
46 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐵 ≤ 𝑌 ) → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
47 41 45 46 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
48 40 47 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
50 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D 𝐹 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
51 rescncf ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) → ( ( ℝ D 𝐹 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) )
52 49 50 51 sylc ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
53 33 52 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
54 cncff ⊢ ( ( ℝ D 𝐹 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( ℝ D 𝐹 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
55 5 54 syl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
56 55 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D 𝐹 ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
58 57 reseq1d ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) )
59 49 resmptd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
60 58 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
61 33 60 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
62 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
63 62 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
64 fvexd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
65 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D 𝐹 ) ∈ 𝐿1 )
66 57 65 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿1 )
67 49 63 64 66 iblss ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿1 )
68 61 67 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ∈ 𝐿1 )
69 iccss2 ⊢ ( ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝑋 [,] 𝑌 ) )
70 3 4 69 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝑋 [,] 𝑌 ) )
71 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( 𝐹 ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
72 70 7 71 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
74 13 15 8 53 68 73 ftc2 ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) )
75 33 fveq1d ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑡 ) )
76 fvres ⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
77 75 76 sylan9eq ⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
78 77 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
79 13 rexrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ* )
80 15 rexrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ* )
81 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
82 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
83 fvres ⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
84 fvres ⊢ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
85 83 84 oveqan12d ⊢ ( ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
86 81 82 85 syl2anc ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
87 79 80 8 86 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
88 74 78 87 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
89 9 88 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )