Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.1 |
. . . . . . . . 9
β’ (π β πΆ β β) |
2 | 1 | recld 15080 |
. . . . . . . 8
β’ (π β (ββπΆ) β
β) |
3 | 2 | recnd 11184 |
. . . . . . 7
β’ (π β (ββπΆ) β
β) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββπΆ) β β) |
5 | | itgmulc2nc.3 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ π΅) β
πΏ1) |
6 | | iblmbf 25135 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ π΅) β πΏ1 β (π₯ β π΄ β¦ π΅) β MblFn) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
8 | | itgmulc2nc.2 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π΅ β π) |
9 | 7, 8 | mbfmptcl 25003 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β π΅ β β) |
10 | 9 | recld 15080 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
11 | 10 | recnd 11184 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
12 | 4, 11 | mulcld 11176 |
. . . . 5
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β β) |
13 | 9 | iblcn 25166 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β
((π₯ β π΄ β¦ (ββπ΅)) β πΏ1
β§ (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1))) |
14 | 5, 13 | mpbid 231 |
. . . . . . 7
β’ (π β ((π₯ β π΄ β¦ (ββπ΅)) β πΏ1 β§ (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1)) |
15 | 14 | simpld 496 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1) |
16 | | itgmulc2nc.m |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) |
17 | | ovexd 7393 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (πΆ Β· π΅) β V) |
18 | 16, 17 | mbfdm2 25004 |
. . . . . . . 8
β’ (π β π΄ β dom vol) |
19 | | fconstmpt 5695 |
. . . . . . . . 9
β’ (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ)) |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (π β (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ))) |
21 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) = (π₯ β π΄ β¦ (ββπ΅))) |
22 | 18, 4, 10, 20, 21 | offval2 7638 |
. . . . . . 7
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
23 | | iblmbf 25135 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ (ββπ΅)) β πΏ1 β
(π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
24 | 15, 23 | syl 17 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
25 | 11 | fmpttd 7064 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (ββπ΅)):π΄βΆβ) |
26 | 24, 2, 25 | mbfmulc2re 25015 |
. . . . . . 7
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
27 | 22, 26 | eqeltrrd 2839 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β MblFn) |
28 | 3, 10, 15, 27 | iblmulc2nc 36146 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β
πΏ1) |
29 | 12, 28 | itgcl 25151 |
. . . 4
β’ (π β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β) |
30 | | ax-icn 11111 |
. . . . 5
β’ i β
β |
31 | 9 | imcld 15081 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
32 | 31 | recnd 11184 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
33 | 4, 32 | mulcld 11176 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β β) |
34 | 14 | simprd 497 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1) |
35 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) = (π₯ β π΄ β¦ (ββπ΅))) |
36 | 18, 4, 31, 20, 35 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
37 | | iblmbf 25135 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ (ββπ΅)) β πΏ1 β
(π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
38 | 34, 37 | syl 17 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
39 | 32 | fmpttd 7064 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (ββπ΅)):π΄βΆβ) |
40 | 38, 2, 39 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
41 | 36, 40 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β MblFn) |
42 | 3, 31, 34, 41 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β
πΏ1) |
43 | 33, 42 | itgcl 25151 |
. . . . 5
β’ (π β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β) |
44 | | mulcl 11136 |
. . . . 5
β’ ((i
β β β§ β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β) β (i Β·
β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) β β) |
45 | 30, 43, 44 | sylancr 588 |
. . . 4
β’ (π β (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) β β) |
46 | 1 | imcld 15081 |
. . . . . . . . 9
β’ (π β (ββπΆ) β
β) |
47 | 46 | recnd 11184 |
. . . . . . . 8
β’ (π β (ββπΆ) β
β) |
48 | 47 | negcld 11500 |
. . . . . . 7
β’ (π β -(ββπΆ) β
β) |
49 | 48 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β -(ββπΆ) β β) |
50 | 49, 32 | mulcld 11176 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (-(ββπΆ) Β· (ββπ΅)) β β) |
51 | | fconstmpt 5695 |
. . . . . . . . 9
β’ (π΄ Γ {-(ββπΆ)}) = (π₯ β π΄ β¦ -(ββπΆ)) |
52 | 51 | a1i 11 |
. . . . . . . 8
β’ (π β (π΄ Γ {-(ββπΆ)}) = (π₯ β π΄ β¦ -(ββπΆ))) |
53 | 18, 49, 31, 52, 35 | offval2 7638 |
. . . . . . 7
β’ (π β ((π΄ Γ {-(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ (-(ββπΆ) Β· (ββπ΅)))) |
54 | 46 | renegcld 11583 |
. . . . . . . 8
β’ (π β -(ββπΆ) β
β) |
55 | 38, 54, 39 | mbfmulc2re 25015 |
. . . . . . 7
β’ (π β ((π΄ Γ {-(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
56 | 53, 55 | eqeltrrd 2839 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (-(ββπΆ) Β· (ββπ΅))) β MblFn) |
57 | 48, 31, 34, 56 | iblmulc2nc 36146 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (-(ββπΆ) Β· (ββπ΅))) β
πΏ1) |
58 | 50, 57 | itgcl 25151 |
. . . 4
β’ (π β β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ β β) |
59 | 47 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (ββπΆ) β β) |
60 | 59, 11 | mulcld 11176 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β β) |
61 | | fconstmpt 5695 |
. . . . . . . . . 10
β’ (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ)) |
62 | 61 | a1i 11 |
. . . . . . . . 9
β’ (π β (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ))) |
63 | 18, 59, 10, 62, 21 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
64 | 24, 46, 25 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
65 | 63, 64 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β MblFn) |
66 | 47, 10, 15, 65 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β
πΏ1) |
67 | 60, 66 | itgcl 25151 |
. . . . 5
β’ (π β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β) |
68 | | mulcl 11136 |
. . . . 5
β’ ((i
β β β§ β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β) β (i Β·
β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) β β) |
69 | 30, 67, 68 | sylancr 588 |
. . . 4
β’ (π β (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) β β) |
70 | 29, 45, 58, 69 | add4d 11384 |
. . 3
β’ (π β ((β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) + (β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) = ((β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) + ((i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)))) |
71 | 30 | a1i 11 |
. . . . . 6
β’ (π β i β
β) |
72 | 71, 47 | mulcld 11176 |
. . . . 5
β’ (π β (i Β·
(ββπΆ)) β
β) |
73 | 8, 5 | itgcl 25151 |
. . . . 5
β’ (π β β«π΄π΅ dπ₯ β β) |
74 | 3, 72, 73 | adddird 11181 |
. . . 4
β’ (π β (((ββπΆ) + (i Β·
(ββπΆ)))
Β· β«π΄π΅ dπ₯) = (((ββπΆ) Β· β«π΄π΅ dπ₯) + ((i Β· (ββπΆ)) Β· β«π΄π΅ dπ₯))) |
75 | 8, 5 | itgcnval 25167 |
. . . . . . 7
β’ (π β β«π΄π΅ dπ₯ = (β«π΄(ββπ΅) dπ₯ + (i Β· β«π΄(ββπ΅) dπ₯))) |
76 | 75 | oveq2d 7374 |
. . . . . 6
β’ (π β ((ββπΆ) Β· β«π΄π΅ dπ₯) = ((ββπΆ) Β· (β«π΄(ββπ΅) dπ₯ + (i Β· β«π΄(ββπ΅) dπ₯)))) |
77 | 10, 15 | itgcl 25151 |
. . . . . . 7
β’ (π β β«π΄(ββπ΅) dπ₯ β β) |
78 | 31, 34 | itgcl 25151 |
. . . . . . . 8
β’ (π β β«π΄(ββπ΅) dπ₯ β β) |
79 | | mulcl 11136 |
. . . . . . . 8
β’ ((i
β β β§ β«π΄(ββπ΅) dπ₯ β β) β (i Β·
β«π΄(ββπ΅) dπ₯) β β) |
80 | 30, 78, 79 | sylancr 588 |
. . . . . . 7
β’ (π β (i Β· β«π΄(ββπ΅) dπ₯) β β) |
81 | 3, 77, 80 | adddid 11180 |
. . . . . 6
β’ (π β ((ββπΆ) Β· (β«π΄(ββπ΅) dπ₯ + (i Β· β«π΄(ββπ΅) dπ₯))) = (((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) + ((ββπΆ) Β· (i Β· β«π΄(ββπ΅) dπ₯)))) |
82 | 3, 10, 15, 27, 2, 10 | itgmulc2nclem2 36148 |
. . . . . . 7
β’ (π β ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) = β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) |
83 | 3, 71, 78 | mul12d 11365 |
. . . . . . . 8
β’ (π β ((ββπΆ) Β· (i Β·
β«π΄(ββπ΅) dπ₯)) = (i Β· ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯))) |
84 | 3, 31, 34, 41, 2, 31 | itgmulc2nclem2 36148 |
. . . . . . . . 9
β’ (π β ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) = β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) |
85 | 84 | oveq2d 7374 |
. . . . . . . 8
β’ (π β (i Β·
((ββπΆ) Β·
β«π΄(ββπ΅) dπ₯)) = (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
86 | 83, 85 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((ββπΆ) Β· (i Β·
β«π΄(ββπ΅) dπ₯)) = (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
87 | 82, 86 | oveq12d 7376 |
. . . . . 6
β’ (π β (((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) + ((ββπΆ) Β· (i Β· β«π΄(ββπ΅) dπ₯))) = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
88 | 76, 81, 87 | 3eqtrd 2781 |
. . . . 5
β’ (π β ((ββπΆ) Β· β«π΄π΅ dπ₯) = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
89 | 75 | oveq2d 7374 |
. . . . . 6
β’ (π β ((i Β·
(ββπΆ)) Β·
β«π΄π΅ dπ₯) = ((i Β· (ββπΆ)) Β· (β«π΄(ββπ΅) dπ₯ + (i Β· β«π΄(ββπ΅) dπ₯)))) |
90 | 72, 77, 80 | adddid 11180 |
. . . . . 6
β’ (π β ((i Β·
(ββπΆ)) Β·
(β«π΄(ββπ΅) dπ₯ + (i Β· β«π΄(ββπ΅) dπ₯))) = (((i Β· (ββπΆ)) Β· β«π΄(ββπ΅) dπ₯) + ((i Β· (ββπΆ)) Β· (i Β·
β«π΄(ββπ΅) dπ₯)))) |
91 | 71, 47, 77 | mulassd 11179 |
. . . . . . . . 9
β’ (π β ((i Β·
(ββπΆ)) Β·
β«π΄(ββπ΅) dπ₯) = (i Β· ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯))) |
92 | 47, 10, 15, 65, 46, 10 | itgmulc2nclem2 36148 |
. . . . . . . . . 10
β’ (π β ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) = β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) |
93 | 92 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β (i Β·
((ββπΆ) Β·
β«π΄(ββπ΅) dπ₯)) = (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
94 | 91, 93 | eqtrd 2777 |
. . . . . . . 8
β’ (π β ((i Β·
(ββπΆ)) Β·
β«π΄(ββπ΅) dπ₯) = (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
95 | 71, 47, 71, 78 | mul4d 11368 |
. . . . . . . . 9
β’ (π β ((i Β·
(ββπΆ)) Β·
(i Β· β«π΄(ββπ΅) dπ₯)) = ((i Β· i) Β·
((ββπΆ) Β·
β«π΄(ββπ΅) dπ₯))) |
96 | | ixi 11785 |
. . . . . . . . . . 11
β’ (i
Β· i) = -1 |
97 | 96 | oveq1i 7368 |
. . . . . . . . . 10
β’ ((i
Β· i) Β· ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯)) = (-1 Β· ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯)) |
98 | 47, 78 | mulcld 11176 |
. . . . . . . . . . 11
β’ (π β ((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) β β) |
99 | 98 | mulm1d 11608 |
. . . . . . . . . 10
β’ (π β (-1 Β·
((ββπΆ) Β·
β«π΄(ββπ΅) dπ₯)) = -((ββπΆ) Β· β«π΄(ββπ΅) dπ₯)) |
100 | 97, 99 | eqtrid 2789 |
. . . . . . . . 9
β’ (π β ((i Β· i) Β·
((ββπΆ) Β·
β«π΄(ββπ΅) dπ₯)) = -((ββπΆ) Β· β«π΄(ββπ΅) dπ₯)) |
101 | 47, 78 | mulneg1d 11609 |
. . . . . . . . . 10
β’ (π β (-(ββπΆ) Β· β«π΄(ββπ΅) dπ₯) = -((ββπΆ) Β· β«π΄(ββπ΅) dπ₯)) |
102 | 48, 31, 34, 56, 54, 31 | itgmulc2nclem2 36148 |
. . . . . . . . . 10
β’ (π β (-(ββπΆ) Β· β«π΄(ββπ΅) dπ₯) = β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) |
103 | 101, 102 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π β -((ββπΆ) Β· β«π΄(ββπ΅) dπ₯) = β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) |
104 | 95, 100, 103 | 3eqtrd 2781 |
. . . . . . . 8
β’ (π β ((i Β·
(ββπΆ)) Β·
(i Β· β«π΄(ββπ΅) dπ₯)) = β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) |
105 | 94, 104 | oveq12d 7376 |
. . . . . . 7
β’ (π β (((i Β·
(ββπΆ)) Β·
β«π΄(ββπ΅) dπ₯) + ((i Β· (ββπΆ)) Β· (i Β·
β«π΄(ββπ΅) dπ₯))) = ((i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯)) |
106 | 69, 58 | addcomd 11358 |
. . . . . . 7
β’ (π β ((i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) = (β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
107 | 105, 106 | eqtrd 2777 |
. . . . . 6
β’ (π β (((i Β·
(ββπΆ)) Β·
β«π΄(ββπ΅) dπ₯) + ((i Β· (ββπΆ)) Β· (i Β·
β«π΄(ββπ΅) dπ₯))) = (β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
108 | 89, 90, 107 | 3eqtrd 2781 |
. . . . 5
β’ (π β ((i Β·
(ββπΆ)) Β·
β«π΄π΅ dπ₯) = (β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
109 | 88, 108 | oveq12d 7376 |
. . . 4
β’ (π β (((ββπΆ) Β· β«π΄π΅ dπ₯) + ((i Β· (ββπΆ)) Β· β«π΄π΅ dπ₯)) = ((β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) + (β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)))) |
110 | 74, 109 | eqtrd 2777 |
. . 3
β’ (π β (((ββπΆ) + (i Β·
(ββπΆ)))
Β· β«π΄π΅ dπ₯) = ((β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) + (β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)))) |
111 | 59, 32 | mulcld 11176 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β β) |
112 | 18, 59, 31, 62, 35 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
113 | 38, 46, 39 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
114 | 112, 113 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β MblFn) |
115 | 47, 31, 34, 114 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅))) β
πΏ1) |
116 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β πΆ β β) |
117 | 116, 9 | mulcld 11176 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (πΆ Β· π΅) β β) |
118 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) = (π₯ β π΄ β¦ (πΆ Β· π΅))) |
119 | | ref 14998 |
. . . . . . . . . . 11
β’
β:ββΆβ |
120 | 119 | a1i 11 |
. . . . . . . . . 10
β’ (π β
β:ββΆβ) |
121 | 120 | feqmptd 6911 |
. . . . . . . . 9
β’ (π β β = (π β β β¦
(ββπ))) |
122 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πΆ Β· π΅) β (ββπ) = (ββ(πΆ Β· π΅))) |
123 | 117, 118,
121, 122 | fmptco 7076 |
. . . . . . . 8
β’ (π β (β β (π₯ β π΄ β¦ (πΆ Β· π΅))) = (π₯ β π΄ β¦ (ββ(πΆ Β· π΅)))) |
124 | 116, 9 | remuld 15104 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (ββ(πΆ Β· π΅)) = (((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅)))) |
125 | 124 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅))))) |
126 | 123, 125 | eqtrd 2777 |
. . . . . . 7
β’ (π β (β β (π₯ β π΄ β¦ (πΆ Β· π΅))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅))))) |
127 | 117 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)):π΄βΆβ) |
128 | | ismbfcn 24996 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ (πΆ Β· π΅)):π΄βΆβ β ((π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn β ((β β
(π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn β§ (β β
(π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn))) |
129 | 127, 128 | syl 17 |
. . . . . . . . 9
β’ (π β ((π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn β ((β β
(π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn β§ (β β
(π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn))) |
130 | 16, 129 | mpbid 231 |
. . . . . . . 8
β’ (π β ((β β (π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn β§ (β β
(π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn)) |
131 | 130 | simpld 496 |
. . . . . . 7
β’ (π β (β β (π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn) |
132 | 126, 131 | eqeltrrd 2839 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅)))) β MblFn) |
133 | 12, 28, 111, 115, 132 | itgsubnc 36143 |
. . . . 5
β’ (π β β«π΄(((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅))) dπ₯ = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
134 | 124 | itgeq2dv 25149 |
. . . . 5
β’ (π β β«π΄(ββ(πΆ Β· π΅)) dπ₯ = β«π΄(((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅))) dπ₯) |
135 | 111, 115 | itgneg 25171 |
. . . . . . . 8
β’ (π β -β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ = β«π΄-((ββπΆ) Β· (ββπ΅)) dπ₯) |
136 | 59, 32 | mulneg1d 11609 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (-(ββπΆ) Β· (ββπ΅)) = -((ββπΆ) Β· (ββπ΅))) |
137 | 136 | itgeq2dv 25149 |
. . . . . . . 8
β’ (π β β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯ = β«π΄-((ββπΆ) Β· (ββπ΅)) dπ₯) |
138 | 135, 137 | eqtr4d 2780 |
. . . . . . 7
β’ (π β -β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ = β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) |
139 | 138 | oveq2d 7374 |
. . . . . 6
β’ (π β (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + -β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯)) |
140 | 111, 115 | itgcl 25151 |
. . . . . . 7
β’ (π β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β) |
141 | 29, 140 | negsubd 11519 |
. . . . . 6
β’ (π β (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + -β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
142 | 139, 141 | eqtr3d 2779 |
. . . . 5
β’ (π β (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ β β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
143 | 133, 134,
142 | 3eqtr4d 2787 |
. . . 4
β’ (π β β«π΄(ββ(πΆ Β· π΅)) dπ₯ = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯)) |
144 | 116, 9 | immuld 15105 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (ββ(πΆ Β· π΅)) = (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅)))) |
145 | 144 | itgeq2dv 25149 |
. . . . . . 7
β’ (π β β«π΄(ββ(πΆ Β· π΅)) dπ₯ = β«π΄(((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅))) dπ₯) |
146 | | imf 14999 |
. . . . . . . . . . . . 13
β’
β:ββΆβ |
147 | 146 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β
β:ββΆβ) |
148 | 147 | feqmptd 6911 |
. . . . . . . . . . 11
β’ (π β β = (π β β β¦
(ββπ))) |
149 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = (πΆ Β· π΅) β (ββπ) = (ββ(πΆ Β· π΅))) |
150 | 117, 118,
148, 149 | fmptco 7076 |
. . . . . . . . . 10
β’ (π β (β β (π₯ β π΄ β¦ (πΆ Β· π΅))) = (π₯ β π΄ β¦ (ββ(πΆ Β· π΅)))) |
151 | 144 | mpteq2dva 5206 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅))))) |
152 | 150, 151 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β (β β (π₯ β π΄ β¦ (πΆ Β· π΅))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅))))) |
153 | 130 | simprd 497 |
. . . . . . . . 9
β’ (π β (β β (π₯ β π΄ β¦ (πΆ Β· π΅))) β MblFn) |
154 | 152, 153 | eqeltrrd 2839 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅)))) β MblFn) |
155 | 33, 42, 60, 66, 154 | itgaddnc 36141 |
. . . . . . 7
β’ (π β β«π΄(((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅))) dπ₯ = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
156 | 145, 155 | eqtrd 2777 |
. . . . . 6
β’ (π β β«π΄(ββ(πΆ Β· π΅)) dπ₯ = (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) |
157 | 156 | oveq2d 7374 |
. . . . 5
β’ (π β (i Β· β«π΄(ββ(πΆ Β· π΅)) dπ₯) = (i Β· (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
158 | 71, 43, 67 | adddid 11180 |
. . . . 5
β’ (π β (i Β· (β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)) = ((i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
159 | 157, 158 | eqtrd 2777 |
. . . 4
β’ (π β (i Β· β«π΄(ββ(πΆ Β· π΅)) dπ₯) = ((i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯))) |
160 | 143, 159 | oveq12d 7376 |
. . 3
β’ (π β (β«π΄(ββ(πΆ Β· π΅)) dπ₯ + (i Β· β«π΄(ββ(πΆ Β· π΅)) dπ₯)) = ((β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯ + β«π΄(-(ββπΆ) Β· (ββπ΅)) dπ₯) + ((i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯) + (i Β· β«π΄((ββπΆ) Β· (ββπ΅)) dπ₯)))) |
161 | 70, 110, 160 | 3eqtr4d 2787 |
. 2
β’ (π β (((ββπΆ) + (i Β·
(ββπΆ)))
Β· β«π΄π΅ dπ₯) = (β«π΄(ββ(πΆ Β· π΅)) dπ₯ + (i Β· β«π΄(ββ(πΆ Β· π΅)) dπ₯))) |
162 | 1 | replimd 15083 |
. . 3
β’ (π β πΆ = ((ββπΆ) + (i Β· (ββπΆ)))) |
163 | 162 | oveq1d 7373 |
. 2
β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = (((ββπΆ) + (i Β· (ββπΆ))) Β· β«π΄π΅ dπ₯)) |
164 | 1, 8, 5, 16 | iblmulc2nc 36146 |
. . 3
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β
πΏ1) |
165 | 117, 164 | itgcnval 25167 |
. 2
β’ (π β β«π΄(πΆ Β· π΅) dπ₯ = (β«π΄(ββ(πΆ Β· π΅)) dπ₯ + (i Β· β«π΄(ββ(πΆ Β· π΅)) dπ₯))) |
166 | 161, 163,
165 | 3eqtr4d 2787 |
1
β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) |