Metamath Proof Explorer

Theorem itgsubstlem

Description: Lemma for itgsubst . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses itgsubst.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
itgsubst.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
itgsubst.le ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
itgsubst.z ⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
itgsubst.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
itgsubst.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) )
itgsubst.b ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
itgsubst.c ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) )
itgsubst.da ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
itgsubst.e ⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
itgsubst.k ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
itgsubst.l ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
itgsubst.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 (,) 𝑊 ) )
itgsubst.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 (,) 𝑊 ) )
itgsubst.cl2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑀 (,) 𝑁 ) )
Assertion itgsubstlem ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgsubst.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 itgsubst.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 itgsubst.le ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
4 itgsubst.z ⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
5 itgsubst.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
6 itgsubst.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) )
7 itgsubst.b ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
8 itgsubst.c ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) )
9 itgsubst.da ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
10 itgsubst.e ⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
11 itgsubst.k ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
12 itgsubst.l ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
13 itgsubst.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 (,) 𝑊 ) )
14 itgsubst.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 (,) 𝑊 ) )
15 itgsubst.cl2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑀 (,) 𝑁 ) )
16 3 ditgpos ⊢ ( 𝜑 → ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 )
17 ax-resscn ⊢ ℝ ⊆ ℂ
18 17 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
19 iccssre ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
20 1 2 19 syl2anc ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
21 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) )
22 eqidd ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) = ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) )
23 oveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝑀 (,) 𝑣 ) = ( 𝑀 (,) 𝐴 ) )
24 itgeq1 ⊢ ( ( 𝑀 (,) 𝑣 ) = ( 𝑀 (,) 𝐴 ) → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 = ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
25 23 24 syl ⊢ ( 𝑣 = 𝐴 → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 = ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
26 15 21 22 25 fmptco ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) )
27 15 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) )
28 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
29 eliooord ⊢ ( 𝑀 ∈ ( 𝑍 (,) 𝑊 ) → ( 𝑍 < 𝑀 ∧ 𝑀 < 𝑊 ) )
30 13 29 syl ⊢ ( 𝜑 → ( 𝑍 < 𝑀 ∧ 𝑀 < 𝑊 ) )
31 30 simpld ⊢ ( 𝜑 → 𝑍 < 𝑀 )
32 eliooord ⊢ ( 𝑁 ∈ ( 𝑍 (,) 𝑊 ) → ( 𝑍 < 𝑁 ∧ 𝑁 < 𝑊 ) )
33 14 32 syl ⊢ ( 𝜑 → ( 𝑍 < 𝑁 ∧ 𝑁 < 𝑊 ) )
34 33 simprd ⊢ ( 𝜑 → 𝑁 < 𝑊 )
35 iccssioo ⊢ ( ( ( 𝑍 ∈ ℝ* ∧ 𝑊 ∈ ℝ* ) ∧ ( 𝑍 < 𝑀 ∧ 𝑁 < 𝑊 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) )
36 4 5 31 34 35 syl22anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) )
37 28 36 sstrid ⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) )
38 ioossre ⊢ ( 𝑍 (,) 𝑊 ) ⊆ ℝ
39 38 a1i ⊢ ( 𝜑 → ( 𝑍 (,) 𝑊 ) ⊆ ℝ )
40 39 17 sstrdi ⊢ ( 𝜑 → ( 𝑍 (,) 𝑊 ) ⊆ ℂ )
41 37 40 sstrd ⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ℂ )
42 cncffvrn ⊢ ( ( ( 𝑀 (,) 𝑁 ) ⊆ ℂ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑀 (,) 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) ) )
43 41 6 42 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑀 (,) 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) ) )
44 27 43 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑀 (,) 𝑁 ) ) )
45 28 sseli ⊢ ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) → 𝑣 ∈ ( 𝑀 [,] 𝑁 ) )
46 38 14 sseldi ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
47 46 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑁 ∈ ℝ* )
49 38 13 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
50 elicc2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁 ) ) )
51 49 46 50 syl2anc ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁 ) ) )
52 51 biimpa ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁 ) )
53 52 simp3d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑣 ≤ 𝑁 )
54 iooss2 ⊢ ( ( 𝑁 ∈ ℝ* ∧ 𝑣 ≤ 𝑁 ) → ( 𝑀 (,) 𝑣 ) ⊆ ( 𝑀 (,) 𝑁 ) )
55 48 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑀 (,) 𝑣 ) ⊆ ( 𝑀 (,) 𝑁 ) )
56 55 sselda ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ) → 𝑢 ∈ ( 𝑀 (,) 𝑁 ) )
57 37 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝑢 ∈ ( 𝑍 (,) 𝑊 ) )
58 cncff ⊢ ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) : ( 𝑍 (,) 𝑊 ) ⟶ ℂ )
59 8 58 syl ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) : ( 𝑍 (,) 𝑊 ) ⟶ ℂ )
60 59 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ) → 𝐶 ∈ ℂ )
61 57 60 syldan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐶 ∈ ℂ )
62 61 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐶 ∈ ℂ )
63 56 62 syldan ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ) → 𝐶 ∈ ℂ )
64 ioombl ⊢ ( 𝑀 (,) 𝑣 ) ∈ dom vol
65 64 a1i ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑀 (,) 𝑣 ) ∈ dom vol )
66 28 a1i ⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) )
67 ioombl ⊢ ( 𝑀 (,) 𝑁 ) ∈ dom vol
68 67 a1i ⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ∈ dom vol )
69 36 sselda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑢 ∈ ( 𝑍 (,) 𝑊 ) )
70 69 60 syldan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐶 ∈ ℂ )
71 36 resmptd ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ↾ ( 𝑀 [,] 𝑁 ) ) = ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) )
72 rescncf ⊢ ( ( 𝑀 [,] 𝑁 ) ⊆ ( 𝑍 (,) 𝑊 ) → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∈ ( ( 𝑍 (,) 𝑊 ) –cn→ ℂ ) → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) ) )
73 36 8 72 sylc ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
74 71 73 eqeltrrd ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
75 cniccibl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) ) → ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
76 49 46 74 75 syl3anc ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
77 66 68 70 76 iblss ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ∈ 𝐿1 )
79 55 65 62 78 iblss ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ↦ 𝐶 ) ∈ 𝐿1 )
80 63 79 itgcl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ∈ ℂ )
81 45 80 sylan2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ∈ ℂ )
82 81 fmpttd ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ )
83 37 38 sstrdi ⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ℝ )
84 fveq2 ⊢ ( 𝑡 = 𝑢 → ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) = ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) )
85 nffvmpt1 ⊢ Ⅎ 𝑢 ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 )
86 nfcv ⊢ Ⅎ 𝑡 ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 )
87 84 85 86 cbvitg ⊢ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) d 𝑢
88 eqid ⊢ ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 )
89 88 fvmpt2 ⊢ ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) = 𝐶 )
90 56 63 89 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ 𝑢 ∈ ( 𝑀 (,) 𝑣 ) ) → ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) = 𝐶 )
91 90 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑢 ) d 𝑢 = ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 )
92 87 91 syl5eq ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ) → ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 )
93 92 mpteq2dva ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) )
94 93 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) ) = ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) )
95 eqid ⊢ ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 )
96 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
97 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
98 lbicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
99 96 97 3 98 syl3anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
100 n0i ⊢ ( 𝑋 ∈ ( 𝑋 [,] 𝑌 ) → ¬ ( 𝑋 [,] 𝑌 ) = ∅ )
101 99 100 syl ⊢ ( 𝜑 → ¬ ( 𝑋 [,] 𝑌 ) = ∅ )
102 feq3 ⊢ ( ( 𝑀 (,) 𝑁 ) = ∅ → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑀 (,) 𝑁 ) ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ ) )
103 27 102 syl5ibcom ⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) = ∅ → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ ) )
104 f00 ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ ↔ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ∅ ∧ ( 𝑋 [,] 𝑌 ) = ∅ ) )
105 104 simprbi ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ∅ → ( 𝑋 [,] 𝑌 ) = ∅ )
106 103 105 syl6 ⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) = ∅ → ( 𝑋 [,] 𝑌 ) = ∅ ) )
107 101 106 mtod ⊢ ( 𝜑 → ¬ ( 𝑀 (,) 𝑁 ) = ∅ )
108 49 rexrd ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
109 ioo0 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( ( 𝑀 (,) 𝑁 ) = ∅ ↔ 𝑁 ≤ 𝑀 ) )
110 108 47 109 syl2anc ⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) = ∅ ↔ 𝑁 ≤ 𝑀 ) )
111 107 110 mtbid ⊢ ( 𝜑 → ¬ 𝑁 ≤ 𝑀 )
112 46 49 letrid ⊢ ( 𝜑 → ( 𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁 ) )
113 112 ord ⊢ ( 𝜑 → ( ¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁 ) )
114 111 113 mpd ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
115 resmpt ⊢ ( ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
116 28 115 ax-mp ⊢ ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 )
117 rescncf ⊢ ( ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) ) )
118 28 74 117 mpsyl ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ↾ ( 𝑀 (,) 𝑁 ) ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
119 116 118 eqeltrrid ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
120 95 49 46 114 119 77 ftc1cn ⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) ( ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ‘ 𝑡 ) d 𝑡 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
121 36 38 sstrdi ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
122 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
123 122 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
124 iccntr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑀 [,] 𝑁 ) ) = ( 𝑀 (,) 𝑁 ) )
125 49 46 124 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑀 [,] 𝑁 ) ) = ( 𝑀 (,) 𝑁 ) )
126 18 121 80 123 122 125 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 [,] 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) )
127 94 120 126 3eqtr3rd ⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
128 127 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = dom ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) )
129 88 61 dmmptd ⊢ ( 𝜑 → dom ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) = ( 𝑀 (,) 𝑁 ) )
130 128 129 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑀 (,) 𝑁 ) )
131 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑀 (,) 𝑁 ) ) → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
132 18 82 83 130 131 syl31anc ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑀 (,) 𝑁 ) –cn→ ℂ ) )
133 44 132 cncfco ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
134 26 133 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
135 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
136 134 135 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
137 136 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ∈ ℂ )
138 iccntr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
139 1 2 138 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
140 18 20 137 123 122 139 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) )
141 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
142 141 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
143 ioossicc ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
144 143 sseli ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) )
145 144 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ ( 𝑀 (,) 𝑁 ) )
146 elin ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) ↔ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 ) )
147 7 146 sylib ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 ) )
148 147 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
149 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
150 148 149 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
151 150 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ℂ )
152 61 fmpttd ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ )
153 nfcv ⊢ Ⅎ 𝑣 𝐶
154 nfcsb1v ⊢ Ⅎ 𝑢 ⦋ 𝑣 / 𝑢 ⦌ 𝐶
155 csbeq1a ⊢ ( 𝑢 = 𝑣 → 𝐶 = ⦋ 𝑣 / 𝑢 ⦌ 𝐶 )
156 153 154 155 cbvmpt ⊢ ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) = ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 )
157 156 fmpt ⊢ ( ∀ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ∈ ℂ ↔ ( 𝑢 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℂ )
158 152 157 sylibr ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ∈ ℂ )
159 158 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ∈ ℂ )
160 38 17 sstri ⊢ ( 𝑍 (,) 𝑊 ) ⊆ ℂ
161 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝑍 (,) 𝑊 ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) )
162 6 161 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) )
163 162 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑍 (,) 𝑊 ) )
164 160 163 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ℂ )
165 18 20 164 123 122 139 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ) )
166 165 9 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
167 127 156 eqtrdi ⊢ ( 𝜑 → ( ℝ D ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ∫ ( 𝑀 (,) 𝑣 ) 𝐶 d 𝑢 ) ) = ( 𝑣 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑣 / 𝑢 ⦌ 𝐶 ) )
168 csbeq1 ⊢ ( 𝑣 = 𝐴 → ⦋ 𝑣 / 𝑢 ⦌ 𝐶 = ⦋ 𝐴 / 𝑢 ⦌ 𝐶 )
169 142 142 145 151 81 159 166 167 25 168 dvmptco ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) ) )
170 nfcvd ⊢ ( 𝐴 ∈ ( 𝑀 (,) 𝑁 ) → Ⅎ 𝑢 𝐸 )
171 170 10 csbiegf ⊢ ( 𝐴 ∈ ( 𝑀 (,) 𝑁 ) → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = 𝐸 )
172 145 171 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝐴 / 𝑢 ⦌ 𝐶 = 𝐸 )
173 172 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) = ( 𝐸 · 𝐵 ) )
174 173 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝐴 / 𝑢 ⦌ 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) )
175 140 169 174 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) )
176 resmpt ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) )
177 143 176 ax-mp ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
178 eqidd ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) = ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) )
179 163 21 178 10 fmptco ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) )
180 6 8 cncfco ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
181 179 180 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
182 rescncf ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) )
183 143 181 182 mpsyl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
184 177 183 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
185 184 148 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
186 175 185 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
187 ioombl ⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
188 187 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
189 fco ⊢ ( ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) : ( 𝑍 (,) 𝑊 ) ⟶ ℂ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝑍 (,) 𝑊 ) ) → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
190 59 162 189 syl2anc ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
191 179 feq1d ⊢ ( 𝜑 → ( ( ( 𝑢 ∈ ( 𝑍 (,) 𝑊 ) ↦ 𝐶 ) ∘ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ ↔ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ ) )
192 190 191 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
193 192 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐸 ∈ ℂ )
194 144 193 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℂ )
195 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) )
196 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
197 188 194 151 195 196 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) )
198 175 197 eqtr4d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) )
199 143 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) )
200 cniccibl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
201 1 2 181 200 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
202 199 188 193 201 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
203 iblmbf ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ MblFn )
204 202 203 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ MblFn )
205 147 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 )
206 cniccbdd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
207 1 2 181 206 syl3anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
208 ssralv ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
209 143 208 ax-mp ⊢ ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
210 eqid ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
211 210 194 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) = ( 𝑋 (,) 𝑌 ) )
212 211 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
213 177 fveq1i ⊢ ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 )
214 fvres ⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ↾ ( 𝑋 (,) 𝑌 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) )
215 213 214 eqtr3id ⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) )
216 215 fveq2d ⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) )
217 216 breq1d ⊢ ( 𝑧 ∈ ( 𝑋 (,) 𝑌 ) → ( ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
218 217 ralbiia ⊢ ( ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
219 212 218 bitr2di ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
220 209 219 syl5ib ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
221 220 reximdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) )
222 207 221 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 )
223 bddmulibl ⊢ ( ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ MblFn ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ 𝐿1 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ( abs ‘ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ‘ 𝑧 ) ) ≤ 𝑦 ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) ∈ 𝐿1 )
224 204 205 222 223 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∘f · ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ) ∈ 𝐿1 )
225 198 224 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ∈ 𝐿1 )
226 1 2 3 186 225 134 ftc2 ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) ) )
227 fveq2 ⊢ ( 𝑡 = 𝑥 → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) = ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) )
228 nfcv ⊢ Ⅎ 𝑥 ℝ
229 nfcv ⊢ Ⅎ 𝑥 D
230 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
231 228 229 230 nfov ⊢ Ⅎ 𝑥 ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) )
232 nfcv ⊢ Ⅎ 𝑥 𝑡
233 231 232 nffv ⊢ Ⅎ 𝑥 ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 )
234 nfcv ⊢ Ⅎ 𝑡 ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 )
235 227 233 234 cbvitg ⊢ ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) d 𝑥
236 175 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ‘ 𝑥 ) )
237 ovex ⊢ ( 𝐸 · 𝐵 ) ∈ V
238 eqid ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) )
239 238 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ∧ ( 𝐸 · 𝐵 ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ‘ 𝑥 ) = ( 𝐸 · 𝐵 ) )
240 237 239 mpan2 ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 · 𝐵 ) ) ‘ 𝑥 ) = ( 𝐸 · 𝐵 ) )
241 236 240 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) = ( 𝐸 · 𝐵 ) )
242 241 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 )
243 235 242 syl5eq ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 )
244 28 15 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ( 𝑀 [,] 𝑁 ) )
245 elicc2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) )
246 49 46 245 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) )
247 246 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) ) )
248 244 247 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁 ) )
249 248 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑀 ≤ 𝐴 )
250 249 ditgpos ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 )
251 250 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) )
252 251 fveq1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑌 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) )
253 ubicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
254 96 97 3 253 syl3anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
255 ditgeq2 ⊢ ( 𝐴 = 𝐿 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
256 12 255 syl ⊢ ( 𝑥 = 𝑌 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
257 eqid ⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 )
258 ditgex ⊢ ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 ∈ V
259 256 257 258 fvmpt ⊢ ( 𝑌 ∈ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑌 ) = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
260 254 259 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑌 ) = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
261 252 260 eqtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) = ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 )
262 251 fveq1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) )
263 ditgeq2 ⊢ ( 𝐴 = 𝐾 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
264 11 263 syl ⊢ ( 𝑥 = 𝑋 → ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
265 ditgex ⊢ ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ∈ V
266 264 257 265 fvmpt ⊢ ( 𝑋 ∈ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑋 ) = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
267 99 266 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⨜ [ 𝑀 → 𝐴 ] 𝐶 d 𝑢 ) ‘ 𝑋 ) = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
268 262 267 eqtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) = ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 )
269 261 268 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) ) = ( ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) )
270 lbicc2 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ( 𝑀 [,] 𝑁 ) )
271 108 47 114 270 syl3anc ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 [,] 𝑁 ) )
272 11 eleq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ 𝐾 ∈ ( 𝑀 [,] 𝑁 ) ) )
273 244 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) 𝐴 ∈ ( 𝑀 [,] 𝑁 ) )
274 272 273 99 rspcdva ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 [,] 𝑁 ) )
275 12 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∈ ( 𝑀 [,] 𝑁 ) ↔ 𝐿 ∈ ( 𝑀 [,] 𝑁 ) ) )
276 275 273 254 rspcdva ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑀 [,] 𝑁 ) )
277 49 46 271 274 276 61 77 ditgsplit ⊢ ( 𝜑 → ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 = ( ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 + ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) )
278 277 oveq1d ⊢ ( 𝜑 → ( ⨜ [ 𝑀 → 𝐿 ] 𝐶 d 𝑢 − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) = ( ( ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 + ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) )
279 49 46 271 274 61 77 ditgcl ⊢ ( 𝜑 → ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ∈ ℂ )
280 49 46 274 276 61 77 ditgcl ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ∈ ℂ )
281 279 280 pncan2d ⊢ ( 𝜑 → ( ( ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 + ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 ) − ⨜ [ 𝑀 → 𝐾 ] 𝐶 d 𝑢 ) = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
282 269 278 281 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ∫ ( 𝑀 (,) 𝐴 ) 𝐶 d 𝑢 ) ‘ 𝑋 ) ) = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
283 226 243 282 3eqtr3d ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 · 𝐵 ) d 𝑥 = ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 )
284 16 283 eqtr2d ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )