MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itgsubstlem Structured version   Visualization version   GIF version

Theorem itgsubstlem 24031
Description: Lemma for itgsubst 24032. (Contributed by Mario Carneiro, 12-Sep-2014.)
Hypotheses
Ref Expression
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
Ref Expression
itgsubstlem (𝜑 → ⨜[𝐾𝐿]𝐶 d𝑢 = ⨜[𝑋𝑌](𝐸 · 𝐵) d𝑥)
Distinct variable groups:   𝑢,𝐸   𝑥,𝑢,𝐾   𝑢,𝑀,𝑥   𝜑,𝑢,𝑥   𝑢,𝑋,𝑥   𝑢,𝑌,𝑥   𝑢,𝐴   𝑥,𝐶   𝑢,𝑊,𝑥   𝑢,𝐿,𝑥   𝑢,𝑁,𝑥   𝑢,𝑍,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥,𝑢)   𝐶(𝑢)   𝐸(𝑥)

Proof of Theorem itgsubstlem
Dummy variables 𝑦 𝑧 𝑡 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itgsubst.le . . 3 (𝜑𝑋𝑌)
21ditgpos 23840 . 2 (𝜑 → ⨜[𝑋𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
3 itgsubst.x . . . 4 (𝜑𝑋 ∈ ℝ)
4 itgsubst.y . . . 4 (𝜑𝑌 ∈ ℝ)
5 ax-resscn 10281 . . . . . . . 8 ℝ ⊆ ℂ
65a1i 11 . . . . . . 7 (𝜑 → ℝ ⊆ ℂ)
7 iccssre 12476 . . . . . . . 8 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
83, 4, 7syl2anc 575 . . . . . . 7 (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
9 itgsubst.cl2 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
10 eqidd 2814 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴))
11 eqidd 2814 . . . . . . . . . . . 12 (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
12 oveq2 6885 . . . . . . . . . . . . 13 (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴))
13 itgeq1 23759 . . . . . . . . . . . . 13 ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
1412, 13syl 17 . . . . . . . . . . . 12 (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
159, 10, 11, 14fmptco 6622 . . . . . . . . . . 11 (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
169fmpttd 6610 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))
17 ioossicc 12480 . . . . . . . . . . . . . . . 16 (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
18 itgsubst.z . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ ℝ*)
19 itgsubst.w . . . . . . . . . . . . . . . . 17 (𝜑𝑊 ∈ ℝ*)
20 itgsubst.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (𝑍(,)𝑊))
21 eliooord 12454 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀𝑀 < 𝑊))
2220, 21syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑍 < 𝑀𝑀 < 𝑊))
2322simpld 484 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 < 𝑀)
24 itgsubst.n . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (𝑍(,)𝑊))
25 eliooord 12454 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁𝑁 < 𝑊))
2624, 25syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑍 < 𝑁𝑁 < 𝑊))
2726simprd 485 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 < 𝑊)
28 iccssioo 12463 . . . . . . . . . . . . . . . . 17 (((𝑍 ∈ ℝ*𝑊 ∈ ℝ*) ∧ (𝑍 < 𝑀𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
2918, 19, 23, 27, 28syl22anc 858 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊))
3017, 29syl5ss 3816 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊))
31 ioossre 12456 . . . . . . . . . . . . . . . . 17 (𝑍(,)𝑊) ⊆ ℝ
3231a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍(,)𝑊) ⊆ ℝ)
3332, 5syl6ss 3817 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍(,)𝑊) ⊆ ℂ)
3430, 33sstrd 3815 . . . . . . . . . . . . . 14 (𝜑 → (𝑀(,)𝑁) ⊆ ℂ)
35 itgsubst.a . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)))
36 cncffvrn 22918 . . . . . . . . . . . . . 14 (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
3734, 35, 36syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)))
3816, 37mpbird 248 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)))
3917sseli 3801 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁))
4031, 24sseldi 3803 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℝ)
4140rexrd 10377 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℝ*)
4241adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈ ℝ*)
4331, 20sseldi 3803 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
44 elicc2 12459 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀𝑣𝑣𝑁)))
4543, 40, 44syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀𝑣𝑣𝑁)))
4645biimpa 464 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀𝑣𝑣𝑁))
4746simp3d 1167 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → 𝑣𝑁)
48 iooss2 12432 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℝ*𝑣𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
4942, 47, 48syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁))
5049sselda 3805 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁))
5130sselda 3805 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
52 itgsubst.c . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ))
53 cncff 22913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
55 eqid 2813 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶)
5655fmpt 6605 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑢 ∈ (𝑍(,)𝑊)𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ)
5754, 56sylibr 225 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑢 ∈ (𝑍(,)𝑊)𝐶 ∈ ℂ)
5857r19.21bi 3127 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ)
5951, 58syldan 581 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
6059adantlr 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ)
6150, 60syldan 581 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ)
62 ioombl 23552 . . . . . . . . . . . . . . . . . 18 (𝑀(,)𝑣) ∈ dom vol
6362a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol)
6417a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁))
65 ioombl 23552 . . . . . . . . . . . . . . . . . . . 20 (𝑀(,)𝑁) ∈ dom vol
6665a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀(,)𝑁) ∈ dom vol)
6729sselda 3805 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊))
6867, 58syldan 581 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ)
6929resmptd 5664 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶))
70 rescncf 22917 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
7129, 52, 70sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
7269, 71eqeltrrd 2893 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ))
73 cniccibl 23827 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿1)
7443, 40, 72, 73syl3anc 1483 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ 𝐿1)
7564, 66, 68, 74iblss 23791 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿1)
7675adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ 𝐿1)
7749, 63, 60, 76iblss 23791 . . . . . . . . . . . . . . . 16 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈ 𝐿1)
7861, 77itgcl 23770 . . . . . . . . . . . . . . 15 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
7939, 78sylan2 582 . . . . . . . . . . . . . 14 ((𝜑𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ)
8079fmpttd 6610 . . . . . . . . . . . . 13 (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ)
8130, 31syl6ss 3817 . . . . . . . . . . . . 13 (𝜑 → (𝑀(,)𝑁) ⊆ ℝ)
82 fveq2 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢))
83 nffvmpt1 6422 . . . . . . . . . . . . . . . . . . . 20 𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡)
84 nfcv 2955 . . . . . . . . . . . . . . . . . . . 20 𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)
8582, 83, 84cbvitg 23762 . . . . . . . . . . . . . . . . . . 19 ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢
86 eqid 2813 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
8786fvmpt2 6515 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
8850, 61, 87syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶)
8988itgeq2dv 23768 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
9085, 89syl5eq 2859 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢)
9190mpteq2dva 4945 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))
9291oveq2d 6893 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
93 eqid 2813 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)
943rexrd 10377 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 ∈ ℝ*)
954rexrd 10377 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 ∈ ℝ*)
96 lbicc2 12511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
9794, 95, 1, 96syl3anc 1483 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ (𝑋[,]𝑌))
98 n0i 4128 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ (𝑋[,]𝑌) = ∅)
100 feq3 6242 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
10116, 100syl5ibcom 236 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅))
102 f00 6305 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅))
103102simprbi 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅)
104101, 103syl6 35 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅))
10599, 104mtod 189 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑀(,)𝑁) = ∅)
10643rexrd 10377 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ*)
107 ioo0 12421 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℝ*𝑁 ∈ ℝ*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁𝑀))
108106, 41, 107syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁𝑀))
109105, 108mtbid 315 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ 𝑁𝑀)
11040, 43letrid 10477 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁𝑀𝑀𝑁))
111110ord 882 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 𝑁𝑀𝑀𝑁))
112109, 111mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑𝑀𝑁)
113 resmpt 5661 . . . . . . . . . . . . . . . . . . 19 ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
11417, 113ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)
115 rescncf 22917 . . . . . . . . . . . . . . . . . . 19 ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)))
11617, 72, 115mpsyl 68 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))
117114, 116syl5eqelr 2897 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ))
11893, 43, 40, 112, 117, 75ftc1cn 24026 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
11929, 31syl6ss 3817 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
120 eqid 2813 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
121120tgioo2 22823 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
122 iccntr 22841 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
12343, 40, 122syl2anc 575 . . . . . . . . . . . . . . . . 17 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁))
1246, 119, 78, 121, 120, 123dvmptntr 23954 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)))
12592, 118, 1243eqtr3rd 2856 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
126125dmeqd 5534 . . . . . . . . . . . . . 14 (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶))
12786, 59dmmptd 6238 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁))
128126, 127eqtrd 2847 . . . . . . . . . . . . 13 (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁))
129 dvcn 23904 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
1306, 80, 81, 128, 129syl31anc 1485 . . . . . . . . . . . 12 (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ))
13138, 130cncfco 22927 . . . . . . . . . . 11 (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
13215, 131eqeltrrd 2893 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ))
133 cncff 22913 . . . . . . . . . 10 ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
134132, 133syl 17 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
135 eqid 2813 . . . . . . . . . 10 (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
136135fmpt 6605 . . . . . . . . 9 (∀𝑥 ∈ (𝑋[,]𝑌)∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ)
137134, 136sylibr 225 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
138137r19.21bi 3127 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ)
139 iccntr 22841 . . . . . . . 8 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
1403, 4, 139syl2anc 575 . . . . . . 7 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌))
1416, 8, 138, 121, 120, 140dvmptntr 23954 . . . . . 6 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)))
142 reelprrecn 10316 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
143142a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
144 ioossicc 12480 . . . . . . . . 9 (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
145144sseli 3801 . . . . . . . 8 (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌))
146145, 9sylan2 582 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁))
147 itgsubst.b . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1))
148 elin 4002 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1) ↔ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1))
149147, 148sylib 209 . . . . . . . . . . 11 (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1))
150149simpld 484 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ))
151 cncff 22913 . . . . . . . . . 10 ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
152150, 151syl 17 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
153 eqid 2813 . . . . . . . . . 10 (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)
154153fmpt 6605 . . . . . . . . 9 (∀𝑥 ∈ (𝑋(,)𝑌)𝐵 ∈ ℂ ↔ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ)
155152, 154sylibr 225 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)𝐵 ∈ ℂ)
156155r19.21bi 3127 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ)
15759fmpttd 6610 . . . . . . . . 9 (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
158 nfcv 2955 . . . . . . . . . . 11 𝑣𝐶
159 nfcsb1v 3751 . . . . . . . . . . 11 𝑢𝑣 / 𝑢𝐶
160 csbeq1a 3744 . . . . . . . . . . 11 (𝑢 = 𝑣𝐶 = 𝑣 / 𝑢𝐶)
161158, 159, 160cbvmpt 4950 . . . . . . . . . 10 (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ 𝑣 / 𝑢𝐶)
162161fmpt 6605 . . . . . . . . 9 (∀𝑣 ∈ (𝑀(,)𝑁)𝑣 / 𝑢𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ)
163157, 162sylibr 225 . . . . . . . 8 (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)𝑣 / 𝑢𝐶 ∈ ℂ)
164163r19.21bi 3127 . . . . . . 7 ((𝜑𝑣 ∈ (𝑀(,)𝑁)) → 𝑣 / 𝑢𝐶 ∈ ℂ)
16531, 5sstri 3814 . . . . . . . . . 10 (𝑍(,)𝑊) ⊆ ℂ
166 cncff 22913 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
16735, 166syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
168 eqid 2813 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)
169168fmpt 6605 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑍(,)𝑊) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊))
170167, 169sylibr 225 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑍(,)𝑊))
171170r19.21bi 3127 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊))
172165, 171sseldi 3803 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ)
1736, 8, 172, 121, 120, 140dvmptntr 23954 . . . . . . . 8 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)))
174 itgsubst.da . . . . . . . 8 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
175173, 174eqtr3d 2849 . . . . . . 7 (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
176125, 161syl6eq 2863 . . . . . . 7 (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ 𝑣 / 𝑢𝐶))
177 csbeq1 3738 . . . . . . 7 (𝑣 = 𝐴𝑣 / 𝑢𝐶 = 𝐴 / 𝑢𝐶)
178143, 143, 146, 156, 79, 164, 175, 176, 14, 177dvmptco 23955 . . . . . 6 (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 / 𝑢𝐶 · 𝐵)))
179 nfcvd 2956 . . . . . . . . . 10 (𝐴 ∈ (𝑀(,)𝑁) → 𝑢𝐸)
180 itgsubst.e . . . . . . . . . 10 (𝑢 = 𝐴𝐶 = 𝐸)
181179, 180csbiegf 3759 . . . . . . . . 9 (𝐴 ∈ (𝑀(,)𝑁) → 𝐴 / 𝑢𝐶 = 𝐸)
182146, 181syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 / 𝑢𝐶 = 𝐸)
183182oveq1d 6892 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → (𝐴 / 𝑢𝐶 · 𝐵) = (𝐸 · 𝐵))
184183mpteq2dva 4945 . . . . . 6 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐴 / 𝑢𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
185141, 178, 1843eqtrd 2851 . . . . 5 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
186 resmpt 5661 . . . . . . . 8 ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
187144, 186ax-mp 5 . . . . . . 7 ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
188 eqidd 2814 . . . . . . . . . 10 (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶))
189171, 10, 188, 180fmptco 6622 . . . . . . . . 9 (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸))
19035, 52cncfco 22927 . . . . . . . . 9 (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ))
191189, 190eqeltrrd 2893 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ))
192 rescncf 22917 . . . . . . . 8 ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
193144, 191, 192mpsyl 68 . . . . . . 7 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
194187, 193syl5eqelr 2897 . . . . . 6 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
195194, 150mulcncf 23433 . . . . 5 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
196185, 195eqeltrd 2892 . . . 4 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
197 ioombl 23552 . . . . . . . 8 (𝑋(,)𝑌) ∈ dom vol
198197a1i 11 . . . . . . 7 (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
199 fco 6276 . . . . . . . . . . . 12 (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
20054, 167, 199syl2anc 575 . . . . . . . . . . 11 (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ)
201189feq1d 6244 . . . . . . . . . . 11 (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ))
202200, 201mpbid 223 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
203 eqid 2813 . . . . . . . . . . 11 (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)
204203fmpt 6605 . . . . . . . . . 10 (∀𝑥 ∈ (𝑋[,]𝑌)𝐸 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)
205202, 204sylibr 225 . . . . . . . . 9 (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐸 ∈ ℂ)
206205r19.21bi 3127 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ)
207145, 206sylan2 582 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ)
208 eqidd 2814 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸))
209 eqidd 2814 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))
210198, 207, 156, 208, 209offval2 7147 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)))
211185, 210eqtr4d 2850 . . . . 5 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)))
212144a1i 11 . . . . . . . 8 (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
213 cniccibl 23827 . . . . . . . . 9 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿1)
2143, 4, 191, 213syl3anc 1483 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ 𝐿1)
215212, 198, 206, 214iblss 23791 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿1)
216 iblmbf 23754 . . . . . . 7 ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿1 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
217215, 216syl 17 . . . . . 6 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn)
218149simprd 485 . . . . . 6 (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1)
219 cniccbdd 23448 . . . . . . . 8 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
2203, 4, 191, 219syl3anc 1483 . . . . . . 7 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
221 ssralv 3870 . . . . . . . . . 10 ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
222144, 221ax-mp 5 . . . . . . . . 9 (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
223 eqid 2813 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)
224223, 207dmmptd 6238 . . . . . . . . . . 11 (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌))
225224raleqdv 3340 . . . . . . . . . 10 (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
226187fveq1i 6412 . . . . . . . . . . . . . 14 (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)
227 fvres 6430 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
228226, 227syl5eqr 2861 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))
229228fveq2d 6415 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)))
230229breq1d 4861 . . . . . . . . . . 11 (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
231230ralbiia 3174 . . . . . . . . . 10 (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
232225, 231syl6rbb 279 . . . . . . . . 9 (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
233222, 232syl5ib 235 . . . . . . . 8 (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
234233reximdv 3210 . . . . . . 7 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦))
235220, 234mpd 15 . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)
236 bddmulibl 23825 . . . . . 6 (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1 ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿1)
237217, 218, 235, 236syl3anc 1483 . . . . 5 (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 · (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈ 𝐿1)
238211, 237eqeltrd 2892 . . . 4 (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ 𝐿1)
2393, 4, 1, 196, 238, 132ftc2 24027 . . 3 (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)))
240 fveq2 6411 . . . . 5 (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥))
241 nfcv 2955 . . . . . . 7 𝑥
242 nfcv 2955 . . . . . . 7 𝑥 D
243 nfmpt1 4948 . . . . . . 7 𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)
244241, 242, 243nfov 6907 . . . . . 6 𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
245 nfcv 2955 . . . . . 6 𝑥𝑡
246244, 245nffv 6421 . . . . 5 𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡)
247 nfcv 2955 . . . . 5 𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)
248240, 246, 247cbvitg 23762 . . . 4 ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥
249185fveq1d 6413 . . . . . 6 (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥))
250 ovex 6909 . . . . . . 7 (𝐸 · 𝐵) ∈ V
251 eqid 2813 . . . . . . . 8 (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))
252251fvmpt2 6515 . . . . . . 7 ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
253250, 252mpan2 674 . . . . . 6 (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵))
254249, 253sylan9eq 2867 . . . . 5 ((𝜑𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵))
255254itgeq2dv 23768 . . . 4 (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
256248, 255syl5eq 2859 . . 3 (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥)
25717, 9sseldi 3803 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁))
258 elicc2 12459 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀𝐴𝐴𝑁)))
25943, 40, 258syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀𝐴𝐴𝑁)))
260259adantr 468 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀𝐴𝐴𝑁)))
261257, 260mpbid 223 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀𝐴𝐴𝑁))
262261simp2d 1166 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → 𝑀𝐴)
263262ditgpos 23840 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢)
264263mpteq2dva 4945 . . . . . . 7 (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))
265264fveq1d 6413 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌))
266 ubicc2 12512 . . . . . . . 8 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
26794, 95, 1, 266syl3anc 1483 . . . . . . 7 (𝜑𝑌 ∈ (𝑋[,]𝑌))
268 itgsubst.l . . . . . . . . 9 (𝑥 = 𝑌𝐴 = 𝐿)
269 ditgeq2 23833 . . . . . . . . 9 (𝐴 = 𝐿 → ⨜[𝑀𝐴]𝐶 d𝑢 = ⨜[𝑀𝐿]𝐶 d𝑢)
270268, 269syl 17 . . . . . . . 8 (𝑥 = 𝑌 → ⨜[𝑀𝐴]𝐶 d𝑢 = ⨜[𝑀𝐿]𝐶 d𝑢)
271 eqid 2813 . . . . . . . 8 (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)
272 ditgex 23836 . . . . . . . 8 ⨜[𝑀𝐿]𝐶 d𝑢 ∈ V
273270, 271, 272fvmpt 6506 . . . . . . 7 (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀𝐿]𝐶 d𝑢)
274267, 273syl 17 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀𝐿]𝐶 d𝑢)
275265, 274eqtr3d 2849 . . . . 5 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀𝐿]𝐶 d𝑢)
276264fveq1d 6413 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))
277 itgsubst.k . . . . . . . . 9 (𝑥 = 𝑋𝐴 = 𝐾)
278 ditgeq2 23833 . . . . . . . . 9 (𝐴 = 𝐾 → ⨜[𝑀𝐴]𝐶 d𝑢 = ⨜[𝑀𝐾]𝐶 d𝑢)
279277, 278syl 17 . . . . . . . 8 (𝑥 = 𝑋 → ⨜[𝑀𝐴]𝐶 d𝑢 = ⨜[𝑀𝐾]𝐶 d𝑢)
280 ditgex 23836 . . . . . . . 8 ⨜[𝑀𝐾]𝐶 d𝑢 ∈ V
281279, 271, 280fvmpt 6506 . . . . . . 7 (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀𝐾]𝐶 d𝑢)
28297, 281syl 17 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀𝐾]𝐶 d𝑢)
283276, 282eqtr3d 2849 . . . . 5 (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀𝐾]𝐶 d𝑢)
284275, 283oveq12d 6895 . . . 4 (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀𝐿]𝐶 d𝑢 − ⨜[𝑀𝐾]𝐶 d𝑢))
285 lbicc2 12511 . . . . . . 7 ((𝑀 ∈ ℝ*𝑁 ∈ ℝ*𝑀𝑁) → 𝑀 ∈ (𝑀[,]𝑁))
286106, 41, 112, 285syl3anc 1483 . . . . . 6 (𝜑𝑀 ∈ (𝑀[,]𝑁))
287277eleq1d 2877 . . . . . . 7 (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁)))
288257ralrimiva 3161 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁))
289287, 288, 97rspcdva 3515 . . . . . 6 (𝜑𝐾 ∈ (𝑀[,]𝑁))
290268eleq1d 2877 . . . . . . 7 (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁)))
291290, 288, 267rspcdva 3515 . . . . . 6 (𝜑𝐿 ∈ (𝑀[,]𝑁))
29243, 40, 286, 289, 291, 59, 75ditgsplit 23845 . . . . 5 (𝜑 → ⨜[𝑀𝐿]𝐶 d𝑢 = (⨜[𝑀𝐾]𝐶 d𝑢 + ⨜[𝐾𝐿]𝐶 d𝑢))
293292oveq1d 6892 . . . 4 (𝜑 → (⨜[𝑀𝐿]𝐶 d𝑢 − ⨜[𝑀𝐾]𝐶 d𝑢) = ((⨜[𝑀𝐾]𝐶 d𝑢 + ⨜[𝐾𝐿]𝐶 d𝑢) − ⨜[𝑀𝐾]𝐶 d𝑢))
29443, 40, 286, 289, 59, 75ditgcl 23842 . . . . 5 (𝜑 → ⨜[𝑀𝐾]𝐶 d𝑢 ∈ ℂ)
29543, 40, 289, 291, 59, 75ditgcl 23842 . . . . 5 (𝜑 → ⨜[𝐾𝐿]𝐶 d𝑢 ∈ ℂ)
296294, 295pncan2d 10682 . . . 4 (𝜑 → ((⨜[𝑀𝐾]𝐶 d𝑢 + ⨜[𝐾𝐿]𝐶 d𝑢) − ⨜[𝑀𝐾]𝐶 d𝑢) = ⨜[𝐾𝐿]𝐶 d𝑢)
297284, 293, 2963eqtrd 2851 . . 3 (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾𝐿]𝐶 d𝑢)
298239, 256, 2973eqtr3d 2855 . 2 (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾𝐿]𝐶 d𝑢)
2992, 298eqtr2d 2848 1 (𝜑 → ⨜[𝐾𝐿]𝐶 d𝑢 = ⨜[𝑋𝑌](𝐸 · 𝐵) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wral 3103  wrex 3104  Vcvv 3398  csb 3735  cin 3775  wss 3776  c0 4123  {cpr 4379   class class class wbr 4851  cmpt 4930  dom cdm 5318  ran crn 5319  cres 5320  ccom 5322  wf 6100  cfv 6104  (class class class)co 6877  𝑓 cof 7128  cc 10222  cr 10223   + caddc 10227   · cmul 10229  *cxr 10361   < clt 10362  cle 10363  cmin 10554  (,)cioo 12396  [,]cicc 12399  abscabs 14200  TopOpenctopn 16290  topGenctg 16306  fldccnfld 19957  intcnt 21039  cnccncf 22896  volcvol 23450  MblFncmbf 23601  𝐿1cibl 23604  citg 23605  cdit 23830   D cdv 23847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cc 9545  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302  ax-addf 10303  ax-mulf 10304
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-symdif 4049  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-iin 4722  df-disj 4820  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-ofr 7131  df-om 7299  df-1st 7401  df-2nd 7402  df-supp 7533  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-omul 7804  df-er 7982  df-map 8097  df-pm 8098  df-ixp 8149  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-fsupp 8518  df-fi 8559  df-sup 8590  df-inf 8591  df-oi 8657  df-card 9051  df-acn 9054  df-cda 9278  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-4 11369  df-5 11370  df-6 11371  df-7 11372  df-8 11373  df-9 11374  df-n0 11563  df-z 11647  df-dec 11763  df-uz 11908  df-q 12011  df-rp 12050  df-xneg 12165  df-xadd 12166  df-xmul 12167  df-ioo 12400  df-ioc 12401  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-fl 12820  df-mod 12896  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-limsup 14428  df-clim 14445  df-rlim 14446  df-sum 14643  df-struct 16073  df-ndx 16074  df-slot 16075  df-base 16077  df-sets 16078  df-ress 16079  df-plusg 16169  df-mulr 16170  df-starv 16171  df-sca 16172  df-vsca 16173  df-ip 16174  df-tset 16175  df-ple 16176  df-ds 16178  df-unif 16179  df-hom 16180  df-cco 16181  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17954  df-cmn 18399  df-psmet 19949  df-xmet 19950  df-met 19951  df-bl 19952  df-mopn 19953  df-fbas 19954  df-fg 19955  df-cnfld 19958  df-top 20916  df-topon 20933  df-topsp 20955  df-bases 20968  df-cld 21041  df-ntr 21042  df-cls 21043  df-nei 21120  df-lp 21158  df-perf 21159  df-cn 21249  df-cnp 21250  df-haus 21337  df-cmp 21408  df-tx 21583  df-hmeo 21776  df-fil 21867  df-fm 21959  df-flim 21960  df-flf 21961  df-xms 22342  df-ms 22343  df-tms 22344  df-cncf 22898  df-ovol 23451  df-vol 23452  df-mbf 23606  df-itg1 23607  df-itg2 23608  df-ibl 23609  df-itg 23610  df-0p 23657  df-ditg 23831  df-limc 23850  df-dv 23851
This theorem is referenced by:  itgsubst  24032
  Copyright terms: Public domain W3C validator