Step | Hyp | Ref
| Expression |
1 | | itgsubst.le |
. . 3
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
2 | 1 | ditgpos 23426 |
. 2
⊢ (𝜑 → ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
3 | | itgsubst.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
4 | | itgsubst.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
5 | | ax-resscn 9872 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
7 | | iccssre 12126 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) |
8 | 3, 4, 7 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
9 | | itgsubst.cl2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
10 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) |
11 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
12 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → (𝑀(,)𝑣) = (𝑀(,)𝐴)) |
13 | | itgeq1 23345 |
. . . . . . . . . . . . 13
⊢ ((𝑀(,)𝑣) = (𝑀(,)𝐴) → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → ∫(𝑀(,)𝑣)𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
15 | 9, 10, 11, 14 | fmptco 6303 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
16 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) |
17 | 9, 16 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁)) |
18 | | ioossicc 12130 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
19 | | itgsubst.z |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 ∈
ℝ*) |
20 | | itgsubst.w |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑊 ∈
ℝ*) |
21 | | itgsubst.m |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ (𝑍(,)𝑊)) |
22 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑍 < 𝑀 ∧ 𝑀 < 𝑊)) |
24 | 23 | simpld 474 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 < 𝑀) |
25 | | itgsubst.n |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (𝑍(,)𝑊)) |
26 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (𝑍(,)𝑊) → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑍 < 𝑁 ∧ 𝑁 < 𝑊)) |
28 | 27 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 < 𝑊) |
29 | | iccssioo 12113 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 ∈ ℝ*
∧ 𝑊 ∈
ℝ*) ∧ (𝑍 < 𝑀 ∧ 𝑁 < 𝑊)) → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
30 | 19, 20, 24, 28, 29 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝑍(,)𝑊)) |
31 | 18, 30 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑍(,)𝑊)) |
32 | | ioossre 12106 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍(,)𝑊) ⊆ ℝ |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℝ) |
34 | 33, 5 | syl6ss 3580 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍(,)𝑊) ⊆ ℂ) |
35 | 31, 34 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℂ) |
36 | | itgsubst.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) |
37 | | cncffvrn 22509 |
. . . . . . . . . . . . . 14
⊢ (((𝑀(,)𝑁) ⊆ ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊))) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
38 | 35, 36, 37 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁)) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁))) |
39 | 17, 38 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑀(,)𝑁))) |
40 | 18 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ (𝑀(,)𝑁) → 𝑣 ∈ (𝑀[,]𝑁)) |
41 | 32, 25 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℝ) |
42 | 41 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑁 ∈
ℝ*) |
44 | 32, 21 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℝ) |
45 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
46 | 44, 41, 45 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↔ (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
47 | 46 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑣 ∈ ℝ ∧ 𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)) |
48 | 47 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → 𝑣 ≤ 𝑁) |
49 | | iooss2 12082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℝ*
∧ 𝑣 ≤ 𝑁) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
50 | 43, 48, 49 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ⊆ (𝑀(,)𝑁)) |
51 | 50 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝑢 ∈ (𝑀(,)𝑁)) |
52 | 31 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
53 | | itgsubst.c |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ)) |
54 | | cncff 22504 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
56 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) |
57 | 56 | fmpt 6289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑢 ∈
(𝑍(,)𝑊)𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ) |
58 | 55, 57 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑢 ∈ (𝑍(,)𝑊)𝐶 ∈ ℂ) |
59 | 58 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑍(,)𝑊)) → 𝐶 ∈ ℂ) |
60 | 52, 59 | syldan 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
61 | 60 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
62 | 51, 61 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → 𝐶 ∈ ℂ) |
63 | | ioombl 23140 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀(,)𝑣) ∈ dom vol |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑀(,)𝑣) ∈ dom vol) |
65 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)) |
66 | | ioombl 23140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀(,)𝑁) ∈ dom vol |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀(,)𝑁) ∈ dom vol) |
68 | 30 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝑢 ∈ (𝑍(,)𝑊)) |
69 | 68, 59 | syldan 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ) |
70 | 30 | resmptd 5371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) = (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶)) |
71 | | rescncf 22508 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀[,]𝑁) ⊆ (𝑍(,)𝑊) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∈ ((𝑍(,)𝑊)–cn→ℂ) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))) |
72 | 30, 53, 71 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
73 | 70, 72 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
74 | | cniccibl 23413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
75 | 44, 41, 73, 74 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈
𝐿1) |
76 | 65, 67, 69, 75 | iblss 23377 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈
𝐿1) |
78 | 50, 64, 61, 77 | iblss 23377 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → (𝑢 ∈ (𝑀(,)𝑣) ↦ 𝐶) ∈
𝐿1) |
79 | 62, 78 | itgcl 23356 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
80 | 40, 79 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ∫(𝑀(,)𝑣)𝐶 d𝑢 ∈ ℂ) |
81 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) |
82 | 80, 81 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ) |
83 | 31, 32 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ ℝ) |
84 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑢 → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) = ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢)) |
85 | | nffvmpt1 6111 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) |
86 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) |
87 | 84, 85, 86 | cbvitg 23348 |
. . . . . . . . . . . . . . . . . . 19
⊢
∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 |
88 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
89 | 88 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ (𝑀(,)𝑁) ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
90 | 51, 62, 89 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) ∧ 𝑢 ∈ (𝑀(,)𝑣)) → ((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) = 𝐶) |
91 | 90 | itgeq2dv 23354 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑢) d𝑢 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
92 | 87, 91 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀[,]𝑁)) → ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡 = ∫(𝑀(,)𝑣)𝐶 d𝑢) |
93 | 92 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
95 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) = (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡) |
96 | 3 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
97 | 4 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
98 | | lbicc2 12159 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
99 | 96, 97, 1, 98 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
100 | | n0i 3879 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ¬ (𝑋[,]𝑌) = ∅) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ (𝑋[,]𝑌) = ∅) |
102 | | feq3 5941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀(,)𝑁) = ∅ → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑀(,)𝑁) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
103 | 17, 102 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅)) |
104 | | f00 6000 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ ↔ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) = ∅ ∧ (𝑋[,]𝑌) = ∅)) |
105 | 104 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶∅ → (𝑋[,]𝑌) = ∅) |
106 | 103, 105 | syl6 34 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ → (𝑋[,]𝑌) = ∅)) |
107 | 101, 106 | mtod 188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑀(,)𝑁) = ∅) |
108 | 44 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
109 | | ioo0 12071 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ*) → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
110 | 108, 42, 109 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀(,)𝑁) = ∅ ↔ 𝑁 ≤ 𝑀)) |
111 | 107, 110 | mtbid 313 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ 𝑁 ≤ 𝑀) |
112 | 41, 44 | letrid 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 ≤ 𝑀 ∨ 𝑀 ≤ 𝑁)) |
113 | 112 | ord 391 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁)) |
114 | 111, 113 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
115 | | resmpt 5369 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
116 | 18, 115 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) |
117 | | rescncf 22508 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℂ) → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ))) |
118 | 18, 73, 117 | mpsyl 66 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑢 ∈ (𝑀[,]𝑁) ↦ 𝐶) ↾ (𝑀(,)𝑁)) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
119 | 116, 118 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
120 | 95, 44, 41, 114, 119, 76 | ftc1cn 23610 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)((𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)‘𝑡) d𝑡)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
121 | 30, 32 | syl6ss 3580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
122 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
123 | 122 | tgioo2 22414 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
124 | | iccntr 22432 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
125 | 44, 41, 124 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
126 | 6, 121, 79, 123, 122, 125 | dvmptntr 23540 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀[,]𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢))) |
127 | 94, 120, 126 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
128 | 127 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶)) |
129 | 88, 60 | dmmptd 5937 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑀(,)𝑁)) |
130 | 128, 129 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) |
131 | | dvcn 23490 |
. . . . . . . . . . . . 13
⊢
(((ℝ ⊆ ℂ ∧ (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢):(𝑀(,)𝑁)⟶ℂ ∧ (𝑀(,)𝑁) ⊆ ℝ) ∧ dom (ℝ D
(𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑀(,)𝑁)) → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
132 | 6, 82, 83, 130, 131 | syl31anc 1321 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∈ ((𝑀(,)𝑁)–cn→ℂ)) |
133 | 39, 132 | cncfco 22518 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
134 | 15, 133 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
135 | | cncff 22504 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
136 | 134, 135 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
137 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) |
138 | 137 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢):(𝑋[,]𝑌)⟶ℂ) |
139 | 136, 138 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ) |
140 | 139 | r19.21bi 2916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ∫(𝑀(,)𝐴)𝐶 d𝑢 ∈ ℂ) |
141 | | iccntr 22432 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
142 | 3, 4, 141 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑋[,]𝑌)) = (𝑋(,)𝑌)) |
143 | 6, 8, 140, 123, 122, 142 | dvmptntr 23540 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))) |
144 | | reelprrecn 9907 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
145 | 144 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
146 | | ioossicc 12130 |
. . . . . . . . 9
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
147 | 146 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) → 𝑥 ∈ (𝑋[,]𝑌)) |
148 | 147, 9 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐴 ∈ (𝑀(,)𝑁)) |
149 | | itgsubst.b |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩
𝐿1)) |
150 | | elin 3758 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ (((𝑋(,)𝑌)–cn→ℂ) ∩ 𝐿1) ↔
((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
151 | 149, 150 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1)) |
152 | 151 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
153 | | cncff 22504 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
154 | 152, 153 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
155 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) |
156 | 155 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑋(,)𝑌)𝐵 ∈ ℂ ↔ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵):(𝑋(,)𝑌)⟶ℂ) |
157 | 154, 156 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑋(,)𝑌)𝐵 ∈ ℂ) |
158 | 157 | r19.21bi 2916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℂ) |
159 | 60, 88 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
160 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣𝐶 |
161 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢⦋𝑣 / 𝑢⦌𝐶 |
162 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → 𝐶 = ⦋𝑣 / 𝑢⦌𝐶) |
163 | 160, 161,
162 | cbvmpt 4677 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶) |
164 | 163 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ ↔ (𝑢 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℂ) |
165 | 159, 164 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (𝑀(,)𝑁)⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
166 | 165 | r19.21bi 2916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑀(,)𝑁)) → ⦋𝑣 / 𝑢⦌𝐶 ∈ ℂ) |
167 | 32, 5 | sstri 3577 |
. . . . . . . . . 10
⊢ (𝑍(,)𝑊) ⊆ ℂ |
168 | | cncff 22504 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴) ∈ ((𝑋[,]𝑌)–cn→(𝑍(,)𝑊)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
169 | 36, 168 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
170 | 16 | fmpt 6289 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐴 ∈ (𝑍(,)𝑊) ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) |
171 | 169, 170 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑍(,)𝑊)) |
172 | 171 | r19.21bi 2916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑍(,)𝑊)) |
173 | 167, 172 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ ℂ) |
174 | 6, 8, 173, 123, 122, 142 | dvmptntr 23540 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴))) |
175 | | itgsubst.da |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
176 | 174, 175 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
177 | 127, 163 | syl6eq 2660 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑣 ∈ (𝑀(,)𝑁) ↦ ∫(𝑀(,)𝑣)𝐶 d𝑢)) = (𝑣 ∈ (𝑀(,)𝑁) ↦ ⦋𝑣 / 𝑢⦌𝐶)) |
178 | | csbeq1 3502 |
. . . . . . 7
⊢ (𝑣 = 𝐴 → ⦋𝑣 / 𝑢⦌𝐶 = ⦋𝐴 / 𝑢⦌𝐶) |
179 | 145, 145,
148, 158, 80, 166, 176, 177, 14, 178 | dvmptco 23541 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋(,)𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵))) |
180 | | nfcvd 2752 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑀(,)𝑁) → Ⅎ𝑢𝐸) |
181 | | itgsubst.e |
. . . . . . . . . 10
⊢ (𝑢 = 𝐴 → 𝐶 = 𝐸) |
182 | 180, 181 | csbiegf 3523 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑀(,)𝑁) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
183 | 148, 182 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ⦋𝐴 / 𝑢⦌𝐶 = 𝐸) |
184 | 183 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → (⦋𝐴 / 𝑢⦌𝐶 · 𝐵) = (𝐸 · 𝐵)) |
185 | 184 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (⦋𝐴 / 𝑢⦌𝐶 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
186 | 143, 179,
185 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
187 | | resmpt 5369 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
188 | 146, 187 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
189 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) = (𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶)) |
190 | 172, 10, 189, 181 | fmptco 6303 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)) |
191 | 36, 53 | cncfco 22518 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
192 | 190, 191 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
193 | | rescncf 22508 |
. . . . . . . 8
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))) |
194 | 146, 192,
193 | mpsyl 66 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
195 | 188, 194 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
196 | 195, 152 | mulcncf 23023 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
197 | 186, 196 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
198 | | ioombl 23140 |
. . . . . . . 8
⊢ (𝑋(,)𝑌) ∈ dom vol |
199 | 198 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol) |
200 | | fco 5971 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶):(𝑍(,)𝑊)⟶ℂ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴):(𝑋[,]𝑌)⟶(𝑍(,)𝑊)) → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
201 | 55, 169, 200 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ) |
202 | 190 | feq1d 5943 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑢 ∈ (𝑍(,)𝑊) ↦ 𝐶) ∘ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐴)):(𝑋[,]𝑌)⟶ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ)) |
203 | 201, 202 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ) |
204 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) |
205 | 204 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑋[,]𝑌)𝐸 ∈ ℂ ↔ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸):(𝑋[,]𝑌)⟶ℂ) |
206 | 203, 205 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐸 ∈ ℂ) |
207 | 206 | r19.21bi 2916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐸 ∈ ℂ) |
208 | 147, 207 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℂ) |
209 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)) |
210 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) |
211 | 199, 208,
158, 209, 210 | offval2 6812 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))) |
212 | 186, 211 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵))) |
213 | 146 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)) |
214 | | cniccibl 23413 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
215 | 3, 4, 192, 214 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈
𝐿1) |
216 | 213, 199,
207, 215 | iblss 23377 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈
𝐿1) |
217 | | iblmbf 23340 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿1 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
218 | 216, 217 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn) |
219 | 151 | simprd 478 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈
𝐿1) |
220 | | cniccbdd 23037 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ (𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ∈ ((𝑋[,]𝑌)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
221 | 3, 4, 192, 220 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
222 | | ssralv 3629 |
. . . . . . . . . 10
⊢ ((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
223 | 146, 222 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
224 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) |
225 | 224, 208 | dmmptd 5937 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) = (𝑋(,)𝑌)) |
226 | 225 | raleqdv 3121 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
227 | 188 | fveq1i 6104 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) |
228 | | fvres 6117 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸) ↾ (𝑋(,)𝑌))‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
229 | 227, 228 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) |
230 | 229 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋(,)𝑌) → (abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) = (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧))) |
231 | 230 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋(,)𝑌) → ((abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ (abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
232 | 231 | ralbiia 2962 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
(𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
233 | 226, 232 | syl6rbb 276 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ (𝑋(,)𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
234 | 223, 233 | syl5ib 233 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
235 | 234 | reximdv 2999 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝑋[,]𝑌)(abs‘((𝑥 ∈ (𝑋[,]𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦)) |
236 | 221, 235 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) |
237 | | bddmulibl 23411 |
. . . . . 6
⊢ (((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ MblFn ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1 ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ dom (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)(abs‘((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸)‘𝑧)) ≤ 𝑦) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
238 | 218, 219,
236, 237 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∘𝑓 ·
(𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵)) ∈
𝐿1) |
239 | 212, 238 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) ∈
𝐿1) |
240 | 3, 4, 1, 197, 239, 134 | ftc2 23611 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋))) |
241 | | fveq2 6103 |
. . . . 5
⊢ (𝑡 = 𝑥 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) = ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥)) |
242 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥ℝ |
243 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥
D |
244 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢) |
245 | 242, 243,
244 | nfov 6575 |
. . . . . 6
⊢
Ⅎ𝑥(ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
246 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝑡 |
247 | 245, 246 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑥((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) |
248 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑡((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) |
249 | 241, 247,
248 | cbvitg 23348 |
. . . 4
⊢
∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 |
250 | 186 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥)) |
251 | | ovex 6577 |
. . . . . . 7
⊢ (𝐸 · 𝐵) ∈ V |
252 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) = (𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵)) |
253 | 252 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑋(,)𝑌) ∧ (𝐸 · 𝐵) ∈ V) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
254 | 251, 253 | mpan2 703 |
. . . . . 6
⊢ (𝑥 ∈ (𝑋(,)𝑌) → ((𝑥 ∈ (𝑋(,)𝑌) ↦ (𝐸 · 𝐵))‘𝑥) = (𝐸 · 𝐵)) |
255 | 250, 254 | sylan9eq 2664 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → ((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) = (𝐸 · 𝐵)) |
256 | 255 | itgeq2dv 23354 |
. . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑥) d𝑥 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
257 | 249, 256 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ∫(𝑋(,)𝑌)((ℝ D (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢))‘𝑡) d𝑡 = ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥) |
258 | 18, 9 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝐴 ∈ (𝑀[,]𝑁)) |
259 | | elicc2 12109 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
260 | 44, 41, 259 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
261 | 260 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ (𝑀[,]𝑁) ↔ (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁))) |
262 | 258, 261 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → (𝐴 ∈ ℝ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) |
263 | 262 | simp2d 1067 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → 𝑀 ≤ 𝐴) |
264 | 263 | ditgpos 23426 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋[,]𝑌)) → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ∫(𝑀(,)𝐴)𝐶 d𝑢) |
265 | 264 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)) |
266 | 265 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌)) |
267 | | ubicc2 12160 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
268 | 96, 97, 1, 267 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
269 | | itgsubst.l |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → 𝐴 = 𝐿) |
270 | | ditgeq2 23419 |
. . . . . . . . 9
⊢ (𝐴 = 𝐿 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
271 | 269, 270 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
272 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) = (𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢) |
273 | | ditgex 23422 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐿]𝐶 d𝑢 ∈ V |
274 | 271, 272,
273 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
275 | 268, 274 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
276 | 266, 275 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) = ⨜[𝑀 → 𝐿]𝐶 d𝑢) |
277 | 265 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) |
278 | | itgsubst.k |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐾) |
279 | | ditgeq2 23419 |
. . . . . . . . 9
⊢ (𝐴 = 𝐾 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
280 | 278, 279 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ⨜[𝑀 → 𝐴]𝐶 d𝑢 = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
281 | | ditgex 23422 |
. . . . . . . 8
⊢
⨜[𝑀 →
𝐾]𝐶 d𝑢 ∈ V |
282 | 280, 272,
281 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
283 | 99, 282 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ⨜[𝑀 → 𝐴]𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
284 | 277, 283 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋) = ⨜[𝑀 → 𝐾]𝐶 d𝑢) |
285 | 276, 284 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
286 | | lbicc2 12159 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) |
287 | 108, 42, 114, 286 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) |
288 | 258 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁)) |
289 | 278 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐾 ∈ (𝑀[,]𝑁))) |
290 | 289 | rspcv 3278 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁) → 𝐾 ∈ (𝑀[,]𝑁))) |
291 | 99, 288, 290 | sylc 63 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑀[,]𝑁)) |
292 | 269 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝐴 ∈ (𝑀[,]𝑁) ↔ 𝐿 ∈ (𝑀[,]𝑁))) |
293 | 292 | rspcv 3278 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → (∀𝑥 ∈ (𝑋[,]𝑌)𝐴 ∈ (𝑀[,]𝑁) → 𝐿 ∈ (𝑀[,]𝑁))) |
294 | 268, 288,
293 | sylc 63 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (𝑀[,]𝑁)) |
295 | 44, 41, 287, 291, 294, 60, 76 | ditgsplit 23431 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐿]𝐶 d𝑢 = (⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢)) |
296 | 295 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (⨜[𝑀 → 𝐿]𝐶 d𝑢 − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢)) |
297 | 44, 41, 287, 291, 60, 76 | ditgcl 23428 |
. . . . 5
⊢ (𝜑 → ⨜[𝑀 → 𝐾]𝐶 d𝑢 ∈ ℂ) |
298 | 44, 41, 291, 294, 60, 76 | ditgcl 23428 |
. . . . 5
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 ∈ ℂ) |
299 | 297, 298 | pncan2d 10273 |
. . . 4
⊢ (𝜑 → ((⨜[𝑀 → 𝐾]𝐶 d𝑢 + ⨜[𝐾 → 𝐿]𝐶 d𝑢) − ⨜[𝑀 → 𝐾]𝐶 d𝑢) = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
300 | 285, 296,
299 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑌) − ((𝑥 ∈ (𝑋[,]𝑌) ↦ ∫(𝑀(,)𝐴)𝐶 d𝑢)‘𝑋)) = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
301 | 240, 257,
300 | 3eqtr3d 2652 |
. 2
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 · 𝐵) d𝑥 = ⨜[𝐾 → 𝐿]𝐶 d𝑢) |
302 | 2, 301 | eqtr2d 2645 |
1
⊢ (𝜑 → ⨜[𝐾 → 𝐿]𝐶 d𝑢 = ⨜[𝑋 → 𝑌](𝐸 · 𝐵) d𝑥) |