Step | Hyp | Ref
| Expression |
1 | | i1ff 25043 |
. . . . . . . 8
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
2 | 1 | adantr 482 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β πΉ:ββΆβ) |
3 | 2 | ffnd 6670 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β πΉ Fn
β) |
4 | | fnfvelrn 7032 |
. . . . . 6
β’ ((πΉ Fn β β§ π₯ β β) β (πΉβπ₯) β ran πΉ) |
5 | 3, 4 | sylan 581 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π₯ β β)
β (πΉβπ₯) β ran πΉ) |
6 | | i1f0rn 25049 |
. . . . . 6
β’ (πΉ β dom β«1
β 0 β ran πΉ) |
7 | 6 | ad2antrr 725 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π₯ β β)
β 0 β ran πΉ) |
8 | 5, 7 | ifcld 4533 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π₯ β β)
β if(π₯ β π΄, (πΉβπ₯), 0) β ran πΉ) |
9 | | i1fres.1 |
. . . 4
β’ πΊ = (π₯ β β β¦ if(π₯ β π΄, (πΉβπ₯), 0)) |
10 | 8, 9 | fmptd 7063 |
. . 3
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β πΊ:ββΆran
πΉ) |
11 | 2 | frnd 6677 |
. . 3
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β ran πΉ β
β) |
12 | 10, 11 | fssd 6687 |
. 2
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β πΊ:ββΆβ) |
13 | | i1frn 25044 |
. . . 4
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
14 | 13 | adantr 482 |
. . 3
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β ran πΉ β
Fin) |
15 | 10 | frnd 6677 |
. . 3
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β ran πΊ β ran
πΉ) |
16 | 14, 15 | ssfid 9212 |
. 2
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β ran πΊ β
Fin) |
17 | | eleq1w 2821 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (π₯ β π΄ β π§ β π΄)) |
18 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
19 | 17, 18 | ifbieq1d 4511 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β if(π₯ β π΄, (πΉβπ₯), 0) = if(π§ β π΄, (πΉβπ§), 0)) |
20 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’ (πΉβπ§) β V |
21 | | c0ex 11150 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
22 | 20, 21 | ifex 4537 |
. . . . . . . . . . . . 13
β’ if(π§ β π΄, (πΉβπ§), 0) β V |
23 | 19, 9, 22 | fvmpt 6949 |
. . . . . . . . . . . 12
β’ (π§ β β β (πΊβπ§) = if(π§ β π΄, (πΉβπ§), 0)) |
24 | 23 | adantl 483 |
. . . . . . . . . . 11
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β (πΊβπ§) = if(π§ β π΄, (πΉβπ§), 0)) |
25 | 24 | eqeq1d 2739 |
. . . . . . . . . 10
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β ((πΊβπ§) = π¦ β if(π§ β π΄, (πΉβπ§), 0) = π¦)) |
26 | | eldifsni 4751 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (ran πΊ β {0}) β π¦ β 0) |
27 | 26 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β π¦ β 0) |
28 | 27 | necomd 3000 |
. . . . . . . . . . . . 13
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β 0 β
π¦) |
29 | | iffalse 4496 |
. . . . . . . . . . . . . 14
β’ (Β¬
π§ β π΄ β if(π§ β π΄, (πΉβπ§), 0) = 0) |
30 | 29 | neeq1d 3004 |
. . . . . . . . . . . . 13
β’ (Β¬
π§ β π΄ β (if(π§ β π΄, (πΉβπ§), 0) β π¦ β 0 β π¦)) |
31 | 28, 30 | syl5ibrcom 247 |
. . . . . . . . . . . 12
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β (Β¬
π§ β π΄ β if(π§ β π΄, (πΉβπ§), 0) β π¦)) |
32 | 31 | necon4bd 2964 |
. . . . . . . . . . 11
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β
(if(π§ β π΄, (πΉβπ§), 0) = π¦ β π§ β π΄)) |
33 | 32 | pm4.71rd 564 |
. . . . . . . . . 10
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β
(if(π§ β π΄, (πΉβπ§), 0) = π¦ β (π§ β π΄ β§ if(π§ β π΄, (πΉβπ§), 0) = π¦))) |
34 | 25, 33 | bitrd 279 |
. . . . . . . . 9
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β ((πΊβπ§) = π¦ β (π§ β π΄ β§ if(π§ β π΄, (πΉβπ§), 0) = π¦))) |
35 | | iftrue 4493 |
. . . . . . . . . . 11
β’ (π§ β π΄ β if(π§ β π΄, (πΉβπ§), 0) = (πΉβπ§)) |
36 | 35 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π§ β π΄ β (if(π§ β π΄, (πΉβπ§), 0) = π¦ β (πΉβπ§) = π¦)) |
37 | 36 | pm5.32i 576 |
. . . . . . . . 9
β’ ((π§ β π΄ β§ if(π§ β π΄, (πΉβπ§), 0) = π¦) β (π§ β π΄ β§ (πΉβπ§) = π¦)) |
38 | 34, 37 | bitrdi 287 |
. . . . . . . 8
β’ ((((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β ((πΊβπ§) = π¦ β (π§ β π΄ β§ (πΉβπ§) = π¦))) |
39 | 38 | pm5.32da 580 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β ((π§ β β β§ (πΊβπ§) = π¦) β (π§ β β β§ (π§ β π΄ β§ (πΉβπ§) = π¦)))) |
40 | | an12 644 |
. . . . . . 7
β’ ((π§ β β β§ (π§ β π΄ β§ (πΉβπ§) = π¦)) β (π§ β π΄ β§ (π§ β β β§ (πΉβπ§) = π¦))) |
41 | 39, 40 | bitrdi 287 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β ((π§ β β β§ (πΊβπ§) = π¦) β (π§ β π΄ β§ (π§ β β β§ (πΉβπ§) = π¦)))) |
42 | 10 | ffnd 6670 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β πΊ Fn
β) |
43 | 42 | adantr 482 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β πΊ Fn β) |
44 | | fniniseg 7011 |
. . . . . . 7
β’ (πΊ Fn β β (π§ β (β‘πΊ β {π¦}) β (π§ β β β§ (πΊβπ§) = π¦))) |
45 | 43, 44 | syl 17 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (π§ β (β‘πΊ β {π¦}) β (π§ β β β§ (πΊβπ§) = π¦))) |
46 | 3 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β πΉ Fn β) |
47 | | fniniseg 7011 |
. . . . . . . 8
β’ (πΉ Fn β β (π§ β (β‘πΉ β {π¦}) β (π§ β β β§ (πΉβπ§) = π¦))) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (π§ β (β‘πΉ β {π¦}) β (π§ β β β§ (πΉβπ§) = π¦))) |
49 | 48 | anbi2d 630 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β ((π§ β π΄ β§ π§ β (β‘πΉ β {π¦})) β (π§ β π΄ β§ (π§ β β β§ (πΉβπ§) = π¦)))) |
50 | 41, 45, 49 | 3bitr4d 311 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (π§ β (β‘πΊ β {π¦}) β (π§ β π΄ β§ π§ β (β‘πΉ β {π¦})))) |
51 | | elin 3927 |
. . . . 5
β’ (π§ β (π΄ β© (β‘πΉ β {π¦})) β (π§ β π΄ β§ π§ β (β‘πΉ β {π¦}))) |
52 | 50, 51 | bitr4di 289 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (π§ β (β‘πΊ β {π¦}) β π§ β (π΄ β© (β‘πΉ β {π¦})))) |
53 | 52 | eqrdv 2735 |
. . 3
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (β‘πΊ β {π¦}) = (π΄ β© (β‘πΉ β {π¦}))) |
54 | | simplr 768 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β π΄ β dom
vol) |
55 | | i1fima 25045 |
. . . . 5
β’ (πΉ β dom β«1
β (β‘πΉ β {π¦}) β dom vol) |
56 | 55 | ad2antrr 725 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (β‘πΉ β {π¦}) β dom vol) |
57 | | inmbl 24909 |
. . . 4
β’ ((π΄ β dom vol β§ (β‘πΉ β {π¦}) β dom vol) β (π΄ β© (β‘πΉ β {π¦})) β dom vol) |
58 | 54, 56, 57 | syl2anc 585 |
. . 3
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (π΄ β© (β‘πΉ β {π¦})) β dom vol) |
59 | 53, 58 | eqeltrd 2838 |
. 2
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (β‘πΊ β {π¦}) β dom vol) |
60 | 53 | fveq2d 6847 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(volβ(β‘πΊ β {π¦})) = (volβ(π΄ β© (β‘πΉ β {π¦})))) |
61 | | mblvol 24897 |
. . . . 5
β’ ((π΄ β© (β‘πΉ β {π¦})) β dom vol β (volβ(π΄ β© (β‘πΉ β {π¦}))) = (vol*β(π΄ β© (β‘πΉ β {π¦})))) |
62 | 58, 61 | syl 17 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(volβ(π΄ β© (β‘πΉ β {π¦}))) = (vol*β(π΄ β© (β‘πΉ β {π¦})))) |
63 | 60, 62 | eqtrd 2777 |
. . 3
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(volβ(β‘πΊ β {π¦})) = (vol*β(π΄ β© (β‘πΉ β {π¦})))) |
64 | | inss2 4190 |
. . . 4
β’ (π΄ β© (β‘πΉ β {π¦})) β (β‘πΉ β {π¦}) |
65 | | mblss 24898 |
. . . . 5
β’ ((β‘πΉ β {π¦}) β dom vol β (β‘πΉ β {π¦}) β β) |
66 | 56, 65 | syl 17 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β (β‘πΉ β {π¦}) β β) |
67 | | mblvol 24897 |
. . . . . 6
β’ ((β‘πΉ β {π¦}) β dom vol β (volβ(β‘πΉ β {π¦})) = (vol*β(β‘πΉ β {π¦}))) |
68 | 56, 67 | syl 17 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(volβ(β‘πΉ β {π¦})) = (vol*β(β‘πΉ β {π¦}))) |
69 | | i1fima2sn 25047 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π¦ β (ran πΊ β {0})) β
(volβ(β‘πΉ β {π¦})) β β) |
70 | 69 | adantlr 714 |
. . . . 5
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(volβ(β‘πΉ β {π¦})) β β) |
71 | 68, 70 | eqeltrrd 2839 |
. . . 4
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(vol*β(β‘πΉ β {π¦})) β β) |
72 | | ovolsscl 24853 |
. . . 4
β’ (((π΄ β© (β‘πΉ β {π¦})) β (β‘πΉ β {π¦}) β§ (β‘πΉ β {π¦}) β β β§ (vol*β(β‘πΉ β {π¦})) β β) β (vol*β(π΄ β© (β‘πΉ β {π¦}))) β β) |
73 | 64, 66, 71, 72 | mp3an2i 1467 |
. . 3
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(vol*β(π΄ β© (β‘πΉ β {π¦}))) β β) |
74 | 63, 73 | eqeltrd 2838 |
. 2
β’ (((πΉ β dom β«1
β§ π΄ β dom vol)
β§ π¦ β (ran πΊ β {0})) β
(volβ(β‘πΊ β {π¦})) β β) |
75 | 12, 16, 59, 74 | i1fd 25048 |
1
β’ ((πΉ β dom β«1
β§ π΄ β dom vol)
β πΊ β dom
β«1) |