Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.4 |
. . . . . . 7
β’ (π β πΆ β β) |
2 | | max0sub 13116 |
. . . . . . 7
β’ (πΆ β β β (if(0
β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) = πΆ) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β (if(0 β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) = πΆ) |
4 | 3 | oveq1d 7373 |
. . . . 5
β’ (π β ((if(0 β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) Β· π΅) = (πΆ Β· π΅)) |
5 | 4 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π΄) β ((if(0 β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) Β· π΅) = (πΆ Β· π΅)) |
6 | | 0re 11158 |
. . . . . . . 8
β’ 0 β
β |
7 | | ifcl 4532 |
. . . . . . . 8
β’ ((πΆ β β β§ 0 β
β) β if(0 β€ πΆ, πΆ, 0) β β) |
8 | 1, 6, 7 | sylancl 587 |
. . . . . . 7
β’ (π β if(0 β€ πΆ, πΆ, 0) β β) |
9 | 8 | recnd 11184 |
. . . . . 6
β’ (π β if(0 β€ πΆ, πΆ, 0) β β) |
10 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΄) β if(0 β€ πΆ, πΆ, 0) β β) |
11 | 1 | renegcld 11583 |
. . . . . . . 8
β’ (π β -πΆ β β) |
12 | | ifcl 4532 |
. . . . . . . 8
β’ ((-πΆ β β β§ 0 β
β) β if(0 β€ -πΆ, -πΆ, 0) β β) |
13 | 11, 6, 12 | sylancl 587 |
. . . . . . 7
β’ (π β if(0 β€ -πΆ, -πΆ, 0) β β) |
14 | 13 | recnd 11184 |
. . . . . 6
β’ (π β if(0 β€ -πΆ, -πΆ, 0) β β) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΄) β if(0 β€ -πΆ, -πΆ, 0) β β) |
16 | | itgmulc2nc.5 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΅ β β) |
17 | 16 | recnd 11184 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π΅ β β) |
18 | 10, 15, 17 | subdird 11613 |
. . . 4
β’ ((π β§ π₯ β π΄) β ((if(0 β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) Β· π΅) = ((if(0 β€ πΆ, πΆ, 0) Β· π΅) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅))) |
19 | 5, 18 | eqtr3d 2779 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΆ Β· π΅) = ((if(0 β€ πΆ, πΆ, 0) Β· π΅) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅))) |
20 | 19 | itgeq2dv 25149 |
. 2
β’ (π β β«π΄(πΆ Β· π΅) dπ₯ = β«π΄((if(0 β€ πΆ, πΆ, 0) Β· π΅) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)) dπ₯) |
21 | | ovexd 7393 |
. . 3
β’ ((π β§ π₯ β π΄) β (if(0 β€ πΆ, πΆ, 0) Β· π΅) β V) |
22 | | itgmulc2nc.3 |
. . . 4
β’ (π β (π₯ β π΄ β¦ π΅) β
πΏ1) |
23 | | itgmulc2nc.m |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) |
24 | | ovexd 7393 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΆ Β· π΅) β V) |
25 | 23, 24 | mbfdm2 25004 |
. . . . . 6
β’ (π β π΄ β dom vol) |
26 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if(0 β€ πΆ, πΆ, 0) β β) |
27 | | fconstmpt 5695 |
. . . . . . 7
β’ (π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) = (π₯ β π΄ β¦ if(0 β€ πΆ, πΆ, 0)) |
28 | 27 | a1i 11 |
. . . . . 6
β’ (π β (π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) = (π₯ β π΄ β¦ if(0 β€ πΆ, πΆ, 0))) |
29 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅)) |
30 | 25, 26, 16, 28, 29 | offval2 7638 |
. . . . 5
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· π΅))) |
31 | | iblmbf 25135 |
. . . . . . 7
β’ ((π₯ β π΄ β¦ π΅) β πΏ1 β (π₯ β π΄ β¦ π΅) β MblFn) |
32 | 22, 31 | syl 17 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
33 | 17 | fmpttd 7064 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
34 | 32, 8, 33 | mbfmulc2re 25015 |
. . . . 5
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ π΅)) β MblFn) |
35 | 30, 34 | eqeltrrd 2839 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· π΅)) β MblFn) |
36 | 9, 16, 22, 35 | iblmulc2nc 36146 |
. . 3
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· π΅)) β
πΏ1) |
37 | | ovexd 7393 |
. . 3
β’ ((π β§ π₯ β π΄) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅) β V) |
38 | 13 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if(0 β€ -πΆ, -πΆ, 0) β β) |
39 | | fconstmpt 5695 |
. . . . . . 7
β’ (π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) = (π₯ β π΄ β¦ if(0 β€ -πΆ, -πΆ, 0)) |
40 | 39 | a1i 11 |
. . . . . 6
β’ (π β (π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) = (π₯ β π΄ β¦ if(0 β€ -πΆ, -πΆ, 0))) |
41 | 25, 38, 16, 40, 29 | offval2 7638 |
. . . . 5
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· π΅))) |
42 | 32, 13, 33 | mbfmulc2re 25015 |
. . . . 5
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ π΅)) β MblFn) |
43 | 41, 42 | eqeltrrd 2839 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)) β MblFn) |
44 | 14, 16, 22, 43 | iblmulc2nc 36146 |
. . 3
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)) β
πΏ1) |
45 | 19 | mpteq2dva 5206 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) = (π₯ β π΄ β¦ ((if(0 β€ πΆ, πΆ, 0) Β· π΅) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)))) |
46 | 45, 23 | eqeltrrd 2839 |
. . 3
β’ (π β (π₯ β π΄ β¦ ((if(0 β€ πΆ, πΆ, 0) Β· π΅) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅))) β MblFn) |
47 | 21, 36, 37, 44, 46 | itgsubnc 36143 |
. 2
β’ (π β β«π΄((if(0 β€ πΆ, πΆ, 0) Β· π΅) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)) dπ₯ = (β«π΄(if(0 β€ πΆ, πΆ, 0) Β· π΅) dπ₯ β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· π΅) dπ₯)) |
48 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β V) |
49 | | ifcl 4532 |
. . . . . . . 8
β’ ((π΅ β β β§ 0 β
β) β if(0 β€ π΅, π΅, 0) β β) |
50 | 16, 6, 49 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
51 | 16 | iblre 25161 |
. . . . . . . . 9
β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β
((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β πΏ1 β§
(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β
πΏ1))) |
52 | 22, 51 | mpbid 231 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β πΏ1 β§
(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β
πΏ1)) |
53 | 52 | simpld 496 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β
πΏ1) |
54 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) |
55 | 25, 26, 50, 28, 54 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) = (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)))) |
56 | 16, 32 | mbfpos 25018 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) |
57 | 50 | recnd 11184 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
58 | 57 | fmpttd 7064 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)):π΄βΆβ) |
59 | 56, 8, 58 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) β MblFn) |
60 | 55, 59 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0))) β MblFn) |
61 | 9, 50, 53, 60 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0))) β
πΏ1) |
62 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) β V) |
63 | 16 | renegcld 11583 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β -π΅ β β) |
64 | | ifcl 4532 |
. . . . . . . 8
β’ ((-π΅ β β β§ 0 β
β) β if(0 β€ -π΅, -π΅, 0) β β) |
65 | 63, 6, 64 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β if(0 β€ -π΅, -π΅, 0) β β) |
66 | 52 | simprd 497 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β
πΏ1) |
67 | | eqidd 2738 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) = (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) |
68 | 25, 26, 65, 28, 67 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) = (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) |
69 | 16, 32 | mbfneg 25017 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ -π΅) β MblFn) |
70 | 63, 69 | mbfpos 25018 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) |
71 | 65 | recnd 11184 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β if(0 β€ -π΅, -π΅, 0) β β) |
72 | 71 | fmpttd 7064 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)):π΄βΆβ) |
73 | 70, 8, 72 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) β MblFn) |
74 | 68, 73 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) β MblFn) |
75 | 9, 65, 66, 74 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) β
πΏ1) |
76 | | max0sub 13116 |
. . . . . . . . . . . 12
β’ (π΅ β β β (if(0
β€ π΅, π΅, 0) β if(0 β€ -π΅, -π΅, 0)) = π΅) |
77 | 16, 76 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β if(0 β€ -π΅, -π΅, 0)) = π΅) |
78 | 77 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (if(0 β€ πΆ, πΆ, 0) Β· (if(0 β€ π΅, π΅, 0) β if(0 β€ -π΅, -π΅, 0))) = (if(0 β€ πΆ, πΆ, 0) Β· π΅)) |
79 | 10, 57, 71 | subdid 11612 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (if(0 β€ πΆ, πΆ, 0) Β· (if(0 β€ π΅, π΅, 0) β if(0 β€ -π΅, -π΅, 0))) = ((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) |
80 | 78, 79 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (if(0 β€ πΆ, πΆ, 0) Β· π΅) = ((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) |
81 | 80 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (if(0 β€ πΆ, πΆ, 0) Β· π΅)) = (π₯ β π΄ β¦ ((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))))) |
82 | 30, 81 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((π΄ Γ {if(0 β€ πΆ, πΆ, 0)}) βf Β· (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ ((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))))) |
83 | 82, 34 | eqeltrrd 2839 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ ((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) β MblFn) |
84 | 48, 61, 62, 75, 83 | itgsubnc 36143 |
. . . . 5
β’ (π β β«π΄((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) dπ₯ = (β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯ β β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯)) |
85 | 80 | itgeq2dv 25149 |
. . . . 5
β’ (π β β«π΄(if(0 β€ πΆ, πΆ, 0) Β· π΅) dπ₯ = β«π΄((if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) dπ₯) |
86 | 16, 22 | itgreval 25164 |
. . . . . . 7
β’ (π β β«π΄π΅ dπ₯ = (β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯)) |
87 | 86 | oveq2d 7374 |
. . . . . 6
β’ (π β (if(0 β€ πΆ, πΆ, 0) Β· β«π΄π΅ dπ₯) = (if(0 β€ πΆ, πΆ, 0) Β· (β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯))) |
88 | 50, 53 | itgcl 25151 |
. . . . . . 7
β’ (π β β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β) |
89 | 65, 66 | itgcl 25151 |
. . . . . . 7
β’ (π β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯ β β) |
90 | 9, 88, 89 | subdid 11612 |
. . . . . 6
β’ (π β (if(0 β€ πΆ, πΆ, 0) Β· (β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯)) = ((if(0 β€ πΆ, πΆ, 0) Β· β«π΄if(0 β€ π΅, π΅, 0) dπ₯) β (if(0 β€ πΆ, πΆ, 0) Β· β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯))) |
91 | | max1 13105 |
. . . . . . . . 9
β’ ((0
β β β§ πΆ
β β) β 0 β€ if(0 β€ πΆ, πΆ, 0)) |
92 | 6, 1, 91 | sylancr 588 |
. . . . . . . 8
β’ (π β 0 β€ if(0 β€ πΆ, πΆ, 0)) |
93 | | max1 13105 |
. . . . . . . . 9
β’ ((0
β β β§ π΅
β β) β 0 β€ if(0 β€ π΅, π΅, 0)) |
94 | 6, 16, 93 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β 0 β€ if(0 β€ π΅, π΅, 0)) |
95 | 9, 50, 53, 60, 8, 50, 92, 94 | itgmulc2nclem1 36147 |
. . . . . . 7
β’ (π β (if(0 β€ πΆ, πΆ, 0) Β· β«π΄if(0 β€ π΅, π΅, 0) dπ₯) = β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯) |
96 | | max1 13105 |
. . . . . . . . 9
β’ ((0
β β β§ -π΅
β β) β 0 β€ if(0 β€ -π΅, -π΅, 0)) |
97 | 6, 63, 96 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β 0 β€ if(0 β€ -π΅, -π΅, 0)) |
98 | 9, 65, 66, 74, 8, 65, 92, 97 | itgmulc2nclem1 36147 |
. . . . . . 7
β’ (π β (if(0 β€ πΆ, πΆ, 0) Β· β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯) = β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯) |
99 | 95, 98 | oveq12d 7376 |
. . . . . 6
β’ (π β ((if(0 β€ πΆ, πΆ, 0) Β· β«π΄if(0 β€ π΅, π΅, 0) dπ₯) β (if(0 β€ πΆ, πΆ, 0) Β· β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯)) = (β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯ β β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯)) |
100 | 87, 90, 99 | 3eqtrd 2781 |
. . . . 5
β’ (π β (if(0 β€ πΆ, πΆ, 0) Β· β«π΄π΅ dπ₯) = (β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯ β β«π΄(if(0 β€ πΆ, πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯)) |
101 | 84, 85, 100 | 3eqtr4d 2787 |
. . . 4
β’ (π β β«π΄(if(0 β€ πΆ, πΆ, 0) Β· π΅) dπ₯ = (if(0 β€ πΆ, πΆ, 0) Β· β«π΄π΅ dπ₯)) |
102 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β V) |
103 | 25, 38, 50, 40, 54 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) = (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)))) |
104 | 56, 13, 58 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) β MblFn) |
105 | 103, 104 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0))) β MblFn) |
106 | 14, 50, 53, 105 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0))) β
πΏ1) |
107 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) β V) |
108 | 25, 38, 65, 40, 67 | offval2 7638 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) = (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) |
109 | 70, 13, 72 | mbfmulc2re 25015 |
. . . . . . . 8
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) β MblFn) |
110 | 108, 109 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) β MblFn) |
111 | 14, 65, 66, 110 | iblmulc2nc 36146 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) β
πΏ1) |
112 | 77 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (if(0 β€ -πΆ, -πΆ, 0) Β· (if(0 β€ π΅, π΅, 0) β if(0 β€ -π΅, -π΅, 0))) = (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)) |
113 | 15, 57, 71 | subdid 11612 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (if(0 β€ -πΆ, -πΆ, 0) Β· (if(0 β€ π΅, π΅, 0) β if(0 β€ -π΅, -π΅, 0))) = ((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) |
114 | 112, 113 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (if(0 β€ -πΆ, -πΆ, 0) Β· π΅) = ((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) |
115 | 114 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (if(0 β€ -πΆ, -πΆ, 0) Β· π΅)) = (π₯ β π΄ β¦ ((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))))) |
116 | 41, 115 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((π΄ Γ {if(0 β€ -πΆ, -πΆ, 0)}) βf Β· (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ ((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))))) |
117 | 116, 42 | eqeltrrd 2839 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ ((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)))) β MblFn) |
118 | 102, 106,
107, 111, 117 | itgsubnc 36143 |
. . . . 5
β’ (π β β«π΄((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) dπ₯ = (β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯ β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯)) |
119 | 114 | itgeq2dv 25149 |
. . . . 5
β’ (π β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· π΅) dπ₯ = β«π΄((if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) β (if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0))) dπ₯) |
120 | 86 | oveq2d 7374 |
. . . . . 6
β’ (π β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄π΅ dπ₯) = (if(0 β€ -πΆ, -πΆ, 0) Β· (β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯))) |
121 | 14, 88, 89 | subdid 11612 |
. . . . . 6
β’ (π β (if(0 β€ -πΆ, -πΆ, 0) Β· (β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯)) = ((if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄if(0 β€ π΅, π΅, 0) dπ₯) β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯))) |
122 | | max1 13105 |
. . . . . . . . 9
β’ ((0
β β β§ -πΆ
β β) β 0 β€ if(0 β€ -πΆ, -πΆ, 0)) |
123 | 6, 11, 122 | sylancr 588 |
. . . . . . . 8
β’ (π β 0 β€ if(0 β€ -πΆ, -πΆ, 0)) |
124 | 14, 50, 53, 105, 13, 50, 123, 94 | itgmulc2nclem1 36147 |
. . . . . . 7
β’ (π β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄if(0 β€ π΅, π΅, 0) dπ₯) = β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯) |
125 | 14, 65, 66, 110, 13, 65, 123, 97 | itgmulc2nclem1 36147 |
. . . . . . 7
β’ (π β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯) = β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯) |
126 | 124, 125 | oveq12d 7376 |
. . . . . 6
β’ (π β ((if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄if(0 β€ π΅, π΅, 0) dπ₯) β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯)) = (β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯ β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯)) |
127 | 120, 121,
126 | 3eqtrd 2781 |
. . . . 5
β’ (π β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄π΅ dπ₯) = (β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ π΅, π΅, 0)) dπ₯ β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· if(0 β€ -π΅, -π΅, 0)) dπ₯)) |
128 | 118, 119,
127 | 3eqtr4d 2787 |
. . . 4
β’ (π β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· π΅) dπ₯ = (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄π΅ dπ₯)) |
129 | 101, 128 | oveq12d 7376 |
. . 3
β’ (π β (β«π΄(if(0 β€ πΆ, πΆ, 0) Β· π΅) dπ₯ β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· π΅) dπ₯) = ((if(0 β€ πΆ, πΆ, 0) Β· β«π΄π΅ dπ₯) β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄π΅ dπ₯))) |
130 | 16, 22 | itgcl 25151 |
. . . 4
β’ (π β β«π΄π΅ dπ₯ β β) |
131 | 9, 14, 130 | subdird 11613 |
. . 3
β’ (π β ((if(0 β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) Β· β«π΄π΅ dπ₯) = ((if(0 β€ πΆ, πΆ, 0) Β· β«π΄π΅ dπ₯) β (if(0 β€ -πΆ, -πΆ, 0) Β· β«π΄π΅ dπ₯))) |
132 | 3 | oveq1d 7373 |
. . 3
β’ (π β ((if(0 β€ πΆ, πΆ, 0) β if(0 β€ -πΆ, -πΆ, 0)) Β· β«π΄π΅ dπ₯) = (πΆ Β· β«π΄π΅ dπ₯)) |
133 | 129, 131,
132 | 3eqtr2d 2783 |
. 2
β’ (π β (β«π΄(if(0 β€ πΆ, πΆ, 0) Β· π΅) dπ₯ β β«π΄(if(0 β€ -πΆ, -πΆ, 0) Β· π΅) dπ₯) = (πΆ Β· β«π΄π΅ dπ₯)) |
134 | 20, 47, 133 | 3eqtrrd 2782 |
1
β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) |