Step | Hyp | Ref
| Expression |
1 | | i1fima 25058 |
. . . 4
β’ (πΉ β dom β«1
β (β‘πΉ β π΄) β dom vol) |
2 | 1 | adantr 482 |
. . 3
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β π΄) β dom vol) |
3 | | mblvol 24910 |
. . 3
β’ ((β‘πΉ β π΄) β dom vol β (volβ(β‘πΉ β π΄)) = (vol*β(β‘πΉ β π΄))) |
4 | 2, 3 | syl 17 |
. 2
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (volβ(β‘πΉ β π΄)) = (vol*β(β‘πΉ β π΄))) |
5 | | i1ff 25056 |
. . . . . . 7
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β πΉ:ββΆβ) |
7 | | ffun 6676 |
. . . . . 6
β’ (πΉ:ββΆβ β
Fun πΉ) |
8 | | inpreima 7019 |
. . . . . 6
β’ (Fun
πΉ β (β‘πΉ β (π΄ β© ran πΉ)) = ((β‘πΉ β π΄) β© (β‘πΉ β ran πΉ))) |
9 | 6, 7, 8 | 3syl 18 |
. . . . 5
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β (π΄ β© ran πΉ)) = ((β‘πΉ β π΄) β© (β‘πΉ β ran πΉ))) |
10 | | cnvimass 6038 |
. . . . . . 7
β’ (β‘πΉ β π΄) β dom πΉ |
11 | | cnvimarndm 6039 |
. . . . . . 7
β’ (β‘πΉ β ran πΉ) = dom πΉ |
12 | 10, 11 | sseqtrri 3986 |
. . . . . 6
β’ (β‘πΉ β π΄) β (β‘πΉ β ran πΉ) |
13 | | df-ss 3932 |
. . . . . 6
β’ ((β‘πΉ β π΄) β (β‘πΉ β ran πΉ) β ((β‘πΉ β π΄) β© (β‘πΉ β ran πΉ)) = (β‘πΉ β π΄)) |
14 | 12, 13 | mpbi 229 |
. . . . 5
β’ ((β‘πΉ β π΄) β© (β‘πΉ β ran πΉ)) = (β‘πΉ β π΄) |
15 | 9, 14 | eqtr2di 2794 |
. . . 4
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β π΄) = (β‘πΉ β (π΄ β© ran πΉ))) |
16 | | elinel1 4160 |
. . . . . . . . 9
β’ (0 β
(π΄ β© ran πΉ) β 0 β π΄) |
17 | 16 | con3i 154 |
. . . . . . . 8
β’ (Β¬ 0
β π΄ β Β¬ 0
β (π΄ β© ran πΉ)) |
18 | 17 | adantl 483 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β Β¬ 0 β (π΄
β© ran πΉ)) |
19 | | disjsn 4677 |
. . . . . . 7
β’ (((π΄ β© ran πΉ) β© {0}) = β
β Β¬ 0 β
(π΄ β© ran πΉ)) |
20 | 18, 19 | sylibr 233 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β ((π΄ β© ran πΉ) β© {0}) =
β
) |
21 | | inss2 4194 |
. . . . . . . . 9
β’ (π΄ β© ran πΉ) β ran πΉ |
22 | 5 | frnd 6681 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β ran πΉ β
β) |
23 | 21, 22 | sstrid 3960 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (π΄ β© ran πΉ) β
β) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (π΄ β© ran πΉ) β
β) |
25 | | reldisj 4416 |
. . . . . . 7
β’ ((π΄ β© ran πΉ) β β β (((π΄ β© ran πΉ) β© {0}) = β
β (π΄ β© ran πΉ) β (β β
{0}))) |
26 | 24, 25 | syl 17 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (((π΄ β© ran πΉ) β© {0}) = β
β
(π΄ β© ran πΉ) β (β β
{0}))) |
27 | 20, 26 | mpbid 231 |
. . . . 5
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (π΄ β© ran πΉ) β (β β
{0})) |
28 | | imass2 6059 |
. . . . 5
β’ ((π΄ β© ran πΉ) β (β β {0}) β
(β‘πΉ β (π΄ β© ran πΉ)) β (β‘πΉ β (β β
{0}))) |
29 | 27, 28 | syl 17 |
. . . 4
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β (π΄ β© ran πΉ)) β (β‘πΉ β (β β
{0}))) |
30 | 15, 29 | eqsstrd 3987 |
. . 3
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β π΄) β (β‘πΉ β (β β
{0}))) |
31 | | i1fima 25058 |
. . . . 5
β’ (πΉ β dom β«1
β (β‘πΉ β (β β {0})) β dom
vol) |
32 | 31 | adantr 482 |
. . . 4
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β (β β {0})) β dom
vol) |
33 | | mblss 24911 |
. . . 4
β’ ((β‘πΉ β (β β {0})) β dom
vol β (β‘πΉ β (β β {0})) β
β) |
34 | 32, 33 | syl 17 |
. . 3
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (β‘πΉ β (β β {0})) β
β) |
35 | | mblvol 24910 |
. . . . 5
β’ ((β‘πΉ β (β β {0})) β dom
vol β (volβ(β‘πΉ β (β β {0})))
= (vol*β(β‘πΉ β (β β
{0})))) |
36 | 32, 35 | syl 17 |
. . . 4
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (volβ(β‘πΉ β (β β {0}))) =
(vol*β(β‘πΉ β (β β
{0})))) |
37 | | isi1f 25054 |
. . . . . . 7
β’ (πΉ β dom β«1
β (πΉ β MblFn
β§ (πΉ:ββΆβ β§ ran πΉ β Fin β§
(volβ(β‘πΉ β (β β {0}))) β
β))) |
38 | 37 | simprbi 498 |
. . . . . 6
β’ (πΉ β dom β«1
β (πΉ:ββΆβ β§ ran πΉ β Fin β§
(volβ(β‘πΉ β (β β {0}))) β
β)) |
39 | 38 | simp3d 1145 |
. . . . 5
β’ (πΉ β dom β«1
β (volβ(β‘πΉ β (β β {0}))) β
β) |
40 | 39 | adantr 482 |
. . . 4
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (volβ(β‘πΉ β (β β {0}))) β
β) |
41 | 36, 40 | eqeltrrd 2839 |
. . 3
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (vol*β(β‘πΉ β (β β {0}))) β
β) |
42 | | ovolsscl 24866 |
. . 3
β’ (((β‘πΉ β π΄) β (β‘πΉ β (β β {0})) β§ (β‘πΉ β (β β {0})) β
β β§ (vol*β(β‘πΉ β (β β {0})))
β β) β (vol*β(β‘πΉ β π΄)) β β) |
43 | 30, 34, 41, 42 | syl3anc 1372 |
. 2
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (vol*β(β‘πΉ β π΄)) β β) |
44 | 4, 43 | eqeltrd 2838 |
1
β’ ((πΉ β dom β«1
β§ Β¬ 0 β π΄)
β (volβ(β‘πΉ β π΄)) β β) |