Step | Hyp | Ref
| Expression |
1 | | mbff 24911 |
. . . . . . 7
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) |
2 | 1 | ad2antrr 725 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΉ:dom πΉβΆβ) |
3 | 2 | ffnd 6665 |
. . . . 5
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΉ Fn dom πΉ) |
4 | | iblmbf 25054 |
. . . . . . . 8
β’ (πΊ β πΏ1
β πΊ β
MblFn) |
5 | 4 | ad2antlr 726 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΊ β MblFn) |
6 | | mbff 24911 |
. . . . . . 7
β’ (πΊ β MblFn β πΊ:dom πΊβΆβ) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΊ:dom πΊβΆβ) |
8 | 7 | ffnd 6665 |
. . . . 5
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΊ Fn dom πΊ) |
9 | | mbfdm 24912 |
. . . . . 6
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
10 | 9 | ad2antrr 725 |
. . . . 5
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β dom πΉ β dom vol) |
11 | | mbfdm 24912 |
. . . . . 6
β’ (πΊ β MblFn β dom πΊ β dom
vol) |
12 | 5, 11 | syl 17 |
. . . . 5
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β dom πΊ β dom vol) |
13 | | eqid 2738 |
. . . . 5
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
14 | | eqidd 2739 |
. . . . 5
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β dom πΉ) β (πΉβπ§) = (πΉβπ§)) |
15 | | eqidd 2739 |
. . . . 5
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β dom πΊ) β (πΊβπ§) = (πΊβπ§)) |
16 | 3, 8, 10, 12, 13, 14, 15 | offval 7617 |
. . . 4
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (πΉ βf Β· πΊ) = (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§)))) |
17 | | ovexd 7385 |
. . . . 5
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β ((πΉβπ§) Β· (πΊβπ§)) β V) |
18 | | simpll 766 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΉ β MblFn) |
19 | 18, 5 | mbfmul 25013 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (πΉ βf Β· πΊ) β MblFn) |
20 | 16, 19 | eqeltrrd 2840 |
. . . . 5
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§))) β MblFn) |
21 | | absf 15157 |
. . . . . . . . 9
β’
abs:ββΆβ |
22 | 21 | a1i 11 |
. . . . . . . 8
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β
abs:ββΆβ) |
23 | 20, 17 | mbfmptcl 24922 |
. . . . . . . 8
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β ((πΉβπ§) Β· (πΊβπ§)) β β) |
24 | 22, 23 | cofmpt 7073 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (abs β (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§)))) = (π§ β (dom πΉ β© dom πΊ) β¦ (absβ((πΉβπ§) Β· (πΊβπ§))))) |
25 | 23 | fmpttd 7058 |
. . . . . . . 8
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§))):(dom πΉ β© dom πΊ)βΆβ) |
26 | | ax-resscn 11042 |
. . . . . . . . . . 11
β’ β
β β |
27 | | ssid 3965 |
. . . . . . . . . . 11
β’ β
β β |
28 | | cncfss 24184 |
. . . . . . . . . . 11
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
29 | 26, 27, 28 | mp2an 691 |
. . . . . . . . . 10
β’
(ββcnββ)
β (ββcnββ) |
30 | | abscncf 24186 |
. . . . . . . . . 10
β’ abs
β (ββcnββ) |
31 | 29, 30 | sselii 3940 |
. . . . . . . . 9
β’ abs
β (ββcnββ) |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β abs β (ββcnββ)) |
33 | | cncombf 24944 |
. . . . . . . 8
β’ (((π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§))) β MblFn β§ (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§))):(dom πΉ β© dom πΊ)βΆβ β§ abs β
(ββcnββ)) β
(abs β (π§ β (dom
πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§)))) β MblFn) |
34 | 20, 25, 32, 33 | syl3anc 1372 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (abs β (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§)))) β MblFn) |
35 | 24, 34 | eqeltrrd 2840 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ (absβ((πΉβπ§) Β· (πΊβπ§)))) β MblFn) |
36 | 23 | abscld 15256 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ((πΉβπ§) Β· (πΊβπ§))) β β) |
37 | 36 | rexrd 11139 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ((πΉβπ§) Β· (πΊβπ§))) β
β*) |
38 | 23 | absge0d 15264 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β 0 β€ (absβ((πΉβπ§) Β· (πΊβπ§)))) |
39 | | elxrge0 13303 |
. . . . . . . . . . 11
β’
((absβ((πΉβπ§) Β· (πΊβπ§))) β (0[,]+β) β
((absβ((πΉβπ§) Β· (πΊβπ§))) β β* β§ 0 β€
(absβ((πΉβπ§) Β· (πΊβπ§))))) |
40 | 37, 38, 39 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ((πΉβπ§) Β· (πΊβπ§))) β (0[,]+β)) |
41 | | 0e0iccpnf 13305 |
. . . . . . . . . . 11
β’ 0 β
(0[,]+β) |
42 | 41 | a1i 11 |
. . . . . . . . . 10
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ π§ β (dom πΉ β© dom πΊ)) β 0 β
(0[,]+β)) |
43 | 40, 42 | ifclda 4520 |
. . . . . . . . 9
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β
(0[,]+β)) |
44 | 43 | adantr 482 |
. . . . . . . 8
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β β) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β
(0[,]+β)) |
45 | 44 | fmpttd 7058 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))),
0)):ββΆ(0[,]+β)) |
46 | | reex 11076 |
. . . . . . . . . . . . . . 15
β’ β
β V |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β β β
V) |
48 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β π₯ β β) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β MblFn
β§ πΊ β
πΏ1) β§ (π₯ β β β§ βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β§ π§ β β) β π₯ β β) |
50 | | elinel2 4155 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β (dom πΉ β© dom πΊ) β π§ β dom πΊ) |
51 | | ffvelcdm 7028 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ:dom πΊβΆβ β§ π§ β dom πΊ) β (πΊβπ§) β β) |
52 | 7, 50, 51 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (πΊβπ§) β β) |
53 | 52 | abscld 15256 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ(πΊβπ§)) β β) |
54 | 52 | absge0d 15264 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β 0 β€ (absβ(πΊβπ§))) |
55 | | elrege0 13300 |
. . . . . . . . . . . . . . . . 17
β’
((absβ(πΊβπ§)) β (0[,)+β) β
((absβ(πΊβπ§)) β β β§ 0 β€
(absβ(πΊβπ§)))) |
56 | 53, 54, 55 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ(πΊβπ§)) β (0[,)+β)) |
57 | | 0e0icopnf 13304 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
(0[,)+β) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ π§ β (dom πΉ β© dom πΊ)) β 0 β
(0[,)+β)) |
59 | 56, 58 | ifclda 4520 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0) β
(0[,)+β)) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β MblFn
β§ πΊ β
πΏ1) β§ (π₯ β β β§ βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β§ π§ β β) β if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0) β
(0[,)+β)) |
61 | | fconstmpt 5691 |
. . . . . . . . . . . . . . 15
β’ (β
Γ {π₯}) = (π§ β β β¦ π₯) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (β Γ {π₯}) = (π§ β β β¦ π₯)) |
63 | | eqidd 2739 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)) = (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))) |
64 | 47, 49, 60, 62, 63 | offval2 7628 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β ((β Γ {π₯}) βf Β·
(π§ β β β¦
if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))) = (π§ β β β¦ (π₯ Β· if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)))) |
65 | | ovif2 7448 |
. . . . . . . . . . . . . . 15
β’ (π₯ Β· if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)) = if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), (π₯ Β· 0)) |
66 | 48 | recnd 11117 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β π₯ β β) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β π₯ β β) |
68 | 67 | mul01d 11288 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (π₯ Β· 0) = 0) |
69 | 68 | ifeq2d 4505 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), (π₯ Β· 0)) = if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
70 | 65, 69 | eqtrid 2790 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (π₯ Β· if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)) = if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
71 | 70 | mpteq2dv 5206 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (π§ β β β¦ (π₯ Β· if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))) = (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) |
72 | 64, 71 | eqtrd 2778 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β ((β Γ {π₯}) βf Β·
(π§ β β β¦
if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))) = (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) |
73 | 72 | fveq2d 6842 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β
(β«2β((β Γ {π₯}) βf Β· (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)))) = (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)))) |
74 | 59 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β β) β if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0) β
(0[,)+β)) |
75 | 74 | fmpttd 7058 |
. . . . . . . . . . . . 13
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)),
0)):ββΆ(0[,)+β)) |
76 | 75 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)),
0)):ββΆ(0[,)+β)) |
77 | | inss2 4188 |
. . . . . . . . . . . . . . . . . 18
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (dom πΉ β© dom πΊ) β dom πΊ) |
79 | 20, 17 | mbfdm2 24923 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (dom πΉ β© dom πΊ) β dom vol) |
80 | 7 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β dom πΊ) β (πΊβπ§) β β) |
81 | 7 | feqmptd 6906 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΊ = (π§ β dom πΊ β¦ (πΊβπ§))) |
82 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β πΊ β
πΏ1) |
83 | 81, 82 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β dom πΊ β¦ (πΊβπ§)) β
πΏ1) |
84 | 78, 79, 80, 83 | iblss 25091 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ (πΊβπ§)) β
πΏ1) |
85 | 52, 84 | iblabs 25115 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ (absβ(πΊβπ§))) β
πΏ1) |
86 | 53, 54 | iblpos 25079 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β ((π§ β (dom πΉ β© dom πΊ) β¦ (absβ(πΊβπ§))) β πΏ1 β
((π§ β (dom πΉ β© dom πΊ) β¦ (absβ(πΊβπ§))) β MblFn β§
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ(πΊβπ§)), 0))) β β))) |
87 | 85, 86 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β ((π§ β (dom πΉ β© dom πΊ) β¦ (absβ(πΊβπ§))) β MblFn β§
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ(πΊβπ§)), 0))) β β)) |
88 | 87 | simprd 497 |
. . . . . . . . . . . . 13
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))) β β) |
89 | 88 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ(πΊβπ§)), 0))) β β) |
90 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β π₯ β β) |
91 | | neq0 4304 |
. . . . . . . . . . . . . . 15
β’ (Β¬
(dom πΉ β© dom πΊ) = β
β βπ§ π§ β (dom πΉ β© dom πΊ)) |
92 | | 0re 11091 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β 0 β β) |
94 | | elinel1 4154 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β (dom πΉ β© dom πΊ) β π§ β dom πΉ) |
95 | | ffvelcdm 7028 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:dom πΉβΆβ β§ π§ β dom πΉ) β (πΉβπ§) β β) |
96 | 2, 94, 95 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (πΉβπ§) β β) |
97 | 96 | abscld 15256 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ(πΉβπ§)) β β) |
98 | | simplrl 776 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β π₯ β β) |
99 | 96 | absge0d 15264 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β 0 β€ (absβ(πΉβπ§))) |
100 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) |
101 | | 2fveq3 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π§ β (absβ(πΉβπ¦)) = (absβ(πΉβπ§))) |
102 | 101 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π§ β ((absβ(πΉβπ¦)) β€ π₯ β (absβ(πΉβπ§)) β€ π₯)) |
103 | 102 | rspccva 3579 |
. . . . . . . . . . . . . . . . . . 19
β’
((βπ¦ β
dom πΉ(absβ(πΉβπ¦)) β€ π₯ β§ π§ β dom πΉ) β (absβ(πΉβπ§)) β€ π₯) |
104 | 100, 94, 103 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ(πΉβπ§)) β€ π₯) |
105 | 93, 97, 98, 99, 104 | letrd 11246 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β 0 β€ π₯) |
106 | 105 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β 0 β€ π₯)) |
107 | 106 | exlimdv 1937 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (βπ§ π§ β (dom πΉ β© dom πΊ) β 0 β€ π₯)) |
108 | 91, 107 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (Β¬ (dom πΉ β© dom πΊ) = β
β 0 β€ π₯)) |
109 | 108 | imp 408 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β 0 β€ π₯) |
110 | | elrege0 13300 |
. . . . . . . . . . . . 13
β’ (π₯ β (0[,)+β) β
(π₯ β β β§ 0
β€ π₯)) |
111 | 90, 109, 110 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β π₯ β (0[,)+β)) |
112 | 76, 89, 111 | itg2mulc 25034 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β
(β«2β((β Γ {π₯}) βf Β· (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)))) = (π₯ Β· (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))))) |
113 | 73, 112 | eqtr3d 2780 |
. . . . . . . . . 10
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) = (π₯ Β· (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0))))) |
114 | 90, 89 | remulcld 11119 |
. . . . . . . . . 10
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β (π₯ Β· (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ(πΊβπ§)), 0)))) β β) |
115 | 113, 114 | eqeltrd 2839 |
. . . . . . . . 9
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ (dom πΉ β© dom πΊ) = β
) β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) β β) |
116 | 115 | ex 414 |
. . . . . . . 8
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (Β¬ (dom πΉ β© dom πΊ) = β
β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) β β)) |
117 | | noel 4289 |
. . . . . . . . . . . . . 14
β’ Β¬
π§ β
β
|
118 | | eleq2 2827 |
. . . . . . . . . . . . . 14
β’ ((dom
πΉ β© dom πΊ) = β
β (π§ β (dom πΉ β© dom πΊ) β π§ β β
)) |
119 | 117, 118 | mtbiri 327 |
. . . . . . . . . . . . 13
β’ ((dom
πΉ β© dom πΊ) = β
β Β¬ π§ β (dom πΉ β© dom πΊ)) |
120 | | iffalse 4494 |
. . . . . . . . . . . . 13
β’ (Β¬
π§ β (dom πΉ β© dom πΊ) β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0) = 0) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . 12
β’ ((dom
πΉ β© dom πΊ) = β
β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0) = 0) |
122 | 121 | mpteq2dv 5206 |
. . . . . . . . . . 11
β’ ((dom
πΉ β© dom πΊ) = β
β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) = (π§ β β β¦ 0)) |
123 | | fconstmpt 5691 |
. . . . . . . . . . 11
β’ (β
Γ {0}) = (π§ β
β β¦ 0) |
124 | 122, 123 | eqtr4di 2796 |
. . . . . . . . . 10
β’ ((dom
πΉ β© dom πΊ) = β
β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) = (β Γ
{0})) |
125 | 124 | fveq2d 6842 |
. . . . . . . . 9
β’ ((dom
πΉ β© dom πΊ) = β
β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) = (β«2β(β
Γ {0}))) |
126 | | itg20 25024 |
. . . . . . . . . 10
β’
(β«2β(β Γ {0})) = 0 |
127 | 126, 92 | eqeltri 2835 |
. . . . . . . . 9
β’
(β«2β(β Γ {0})) β
β |
128 | 125, 127 | eqeltrdi 2847 |
. . . . . . . 8
β’ ((dom
πΉ β© dom πΊ) = β
β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) β β) |
129 | 116, 128 | pm2.61d2 181 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) β β) |
130 | 98, 53 | remulcld 11119 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (π₯ Β· (absβ(πΊβπ§))) β β) |
131 | 130 | rexrd 11139 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (π₯ Β· (absβ(πΊβπ§))) β
β*) |
132 | 98, 53, 105, 54 | mulge0d 11666 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β 0 β€ (π₯ Β· (absβ(πΊβπ§)))) |
133 | | elxrge0 13303 |
. . . . . . . . . . . 12
β’ ((π₯ Β· (absβ(πΊβπ§))) β (0[,]+β) β ((π₯ Β· (absβ(πΊβπ§))) β β* β§ 0 β€
(π₯ Β·
(absβ(πΊβπ§))))) |
134 | 131, 132,
133 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (π₯ Β· (absβ(πΊβπ§))) β (0[,]+β)) |
135 | 134, 42 | ifclda 4520 |
. . . . . . . . . 10
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0) β
(0[,]+β)) |
136 | 135 | adantr 482 |
. . . . . . . . 9
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β β) β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0) β
(0[,]+β)) |
137 | 136 | fmpttd 7058 |
. . . . . . . 8
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))),
0)):ββΆ(0[,]+β)) |
138 | 96, 52 | absmuld 15274 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ((πΉβπ§) Β· (πΊβπ§))) = ((absβ(πΉβπ§)) Β· (absβ(πΊβπ§)))) |
139 | | abscl 15098 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβπ§) β β β (absβ(πΊβπ§)) β β) |
140 | | absge0 15107 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβπ§) β β β 0 β€
(absβ(πΊβπ§))) |
141 | 139, 140 | jca 513 |
. . . . . . . . . . . . . . 15
β’ ((πΊβπ§) β β β ((absβ(πΊβπ§)) β β β§ 0 β€
(absβ(πΊβπ§)))) |
142 | 52, 141 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β ((absβ(πΊβπ§)) β β β§ 0 β€
(absβ(πΊβπ§)))) |
143 | | lemul1a 11943 |
. . . . . . . . . . . . . 14
β’
((((absβ(πΉβπ§)) β β β§ π₯ β β β§ ((absβ(πΊβπ§)) β β β§ 0 β€
(absβ(πΊβπ§)))) β§ (absβ(πΉβπ§)) β€ π₯) β ((absβ(πΉβπ§)) Β· (absβ(πΊβπ§))) β€ (π₯ Β· (absβ(πΊβπ§)))) |
144 | 97, 98, 142, 104, 143 | syl31anc 1374 |
. . . . . . . . . . . . 13
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β ((absβ(πΉβπ§)) Β· (absβ(πΊβπ§))) β€ (π₯ Β· (absβ(πΊβπ§)))) |
145 | 138, 144 | eqbrtrd 5126 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β (absβ((πΉβπ§) Β· (πΊβπ§))) β€ (π₯ Β· (absβ(πΊβπ§)))) |
146 | | iftrue 4491 |
. . . . . . . . . . . . 13
β’ (π§ β (dom πΉ β© dom πΊ) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) = (absβ((πΉβπ§) Β· (πΊβπ§)))) |
147 | 146 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) = (absβ((πΉβπ§) Β· (πΊβπ§)))) |
148 | | iftrue 4491 |
. . . . . . . . . . . . 13
β’ (π§ β (dom πΉ β© dom πΊ) β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0) = (π₯ Β· (absβ(πΊβπ§)))) |
149 | 148 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0) = (π₯ Β· (absβ(πΊβπ§)))) |
150 | 145, 147,
149 | 3brtr4d 5136 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ π§ β (dom πΉ β© dom πΊ)) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β€ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
151 | | 0le0 12188 |
. . . . . . . . . . . . . 14
β’ 0 β€
0 |
152 | 151 | a1i 11 |
. . . . . . . . . . . . 13
β’ (Β¬
π§ β (dom πΉ β© dom πΊ) β 0 β€ 0) |
153 | | iffalse 4494 |
. . . . . . . . . . . . 13
β’ (Β¬
π§ β (dom πΉ β© dom πΊ) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) = 0) |
154 | 152, 153,
120 | 3brtr4d 5136 |
. . . . . . . . . . . 12
β’ (Β¬
π§ β (dom πΉ β© dom πΊ) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β€ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
155 | 154 | adantl 483 |
. . . . . . . . . . 11
β’ ((((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β§ Β¬ π§ β (dom πΉ β© dom πΊ)) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β€ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
156 | 150, 155 | pm2.61dan 812 |
. . . . . . . . . 10
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β€ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
157 | 156 | ralrimivw 3146 |
. . . . . . . . 9
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β βπ§ β β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β€ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) |
158 | 46 | a1i 11 |
. . . . . . . . . 10
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β β β V) |
159 | | eqidd 2739 |
. . . . . . . . . 10
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0)) = (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) |
160 | | eqidd 2739 |
. . . . . . . . . 10
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) = (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) |
161 | 158, 44, 136, 159, 160 | ofrfval2 7629 |
. . . . . . . . 9
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β ((π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0)) βr β€ (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)) β βπ§ β β if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0) β€ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) |
162 | 157, 161 | mpbird 257 |
. . . . . . . 8
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0)) βr β€ (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) |
163 | | itg2le 25026 |
. . . . . . . 8
β’ (((π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0)):ββΆ(0[,]+β) β§
(π§ β β β¦
if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)):ββΆ(0[,]+β) β§
(π§ β β β¦
if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0)) βr β€ (π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) β€
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)))) |
164 | 45, 137, 162, 163 | syl3anc 1372 |
. . . . . . 7
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) β€
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)))) |
165 | | itg2lecl 25025 |
. . . . . . 7
β’ (((π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0)):ββΆ(0[,]+β) β§
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0))) β β β§
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) β€
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (π₯ Β· (absβ(πΊβπ§))), 0)))) β
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) β β) |
166 | 45, 129, 164, 165 | syl3anc 1372 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (β«2β(π§ β β β¦ if(π§ β (dom πΉ β© dom πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) β β) |
167 | 36, 38 | iblpos 25079 |
. . . . . 6
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β ((π§ β (dom πΉ β© dom πΊ) β¦ (absβ((πΉβπ§) Β· (πΊβπ§)))) β πΏ1 β
((π§ β (dom πΉ β© dom πΊ) β¦ (absβ((πΉβπ§) Β· (πΊβπ§)))) β MblFn β§
(β«2β(π§
β β β¦ if(π§
β (dom πΉ β© dom
πΊ), (absβ((πΉβπ§) Β· (πΊβπ§))), 0))) β β))) |
168 | 35, 166, 167 | mpbir2and 712 |
. . . . 5
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ (absβ((πΉβπ§) Β· (πΊβπ§)))) β
πΏ1) |
169 | 17, 20, 168 | iblabsr 25116 |
. . . 4
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (π§ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ§) Β· (πΊβπ§))) β
πΏ1) |
170 | 16, 169 | eqeltrd 2839 |
. . 3
β’ (((πΉ β MblFn β§ πΊ β πΏ1)
β§ (π₯ β β
β§ βπ¦ β dom
πΉ(absβ(πΉβπ¦)) β€ π₯)) β (πΉ βf Β· πΊ) β
πΏ1) |
171 | 170 | rexlimdvaa 3152 |
. 2
β’ ((πΉ β MblFn β§ πΊ β πΏ1)
β (βπ₯ β
β βπ¦ β
dom πΉ(absβ(πΉβπ¦)) β€ π₯ β (πΉ βf Β· πΊ) β
πΏ1)) |
172 | 171 | 3impia 1118 |
1
β’ ((πΉ β MblFn β§ πΊ β πΏ1
β§ βπ₯ β
β βπ¦ β
dom πΉ(absβ(πΉβπ¦)) β€ π₯) β (πΉ βf Β· πΊ) β
πΏ1) |