Step | Hyp | Ref
| Expression |
1 | | mbfdm 25006 |
. . 3
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
2 | | fdm 6682 |
. . . 4
β’ (πΉ:π΄βΆβ β dom πΉ = π΄) |
3 | 2 | eleq1d 2823 |
. . 3
β’ (πΉ:π΄βΆβ β (dom πΉ β dom vol β π΄ β dom
vol)) |
4 | 1, 3 | imbitrid 243 |
. 2
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β π΄ β dom vol)) |
5 | | ioomax 13346 |
. . . . 5
β’
(-β(,)+β) = β |
6 | | ioorebas 13375 |
. . . . 5
β’
(-β(,)+β) β ran (,) |
7 | 5, 6 | eqeltrri 2835 |
. . . 4
β’ β
β ran (,) |
8 | | imaeq2 6014 |
. . . . . 6
β’ (π₯ = β β (β‘πΉ β π₯) = (β‘πΉ β β)) |
9 | 8 | eleq1d 2823 |
. . . . 5
β’ (π₯ = β β ((β‘πΉ β π₯) β dom vol β (β‘πΉ β β) β dom
vol)) |
10 | 9 | rspcv 3580 |
. . . 4
β’ (β
β ran (,) β (βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol β (β‘πΉ β β) β dom
vol)) |
11 | 7, 10 | ax-mp 5 |
. . 3
β’
(βπ₯ β
ran (,)(β‘πΉ β π₯) β dom vol β (β‘πΉ β β) β dom
vol) |
12 | | fimacnv 6695 |
. . . 4
β’ (πΉ:π΄βΆβ β (β‘πΉ β β) = π΄) |
13 | 12 | eleq1d 2823 |
. . 3
β’ (πΉ:π΄βΆβ β ((β‘πΉ β β) β dom vol β
π΄ β dom
vol)) |
14 | 11, 13 | imbitrid 243 |
. 2
β’ (πΉ:π΄βΆβ β (βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol β π΄ β dom vol)) |
15 | | ismbf1 25004 |
. . . 4
β’ (πΉ β MblFn β (πΉ β (β
βpm β) β§ βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
16 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’ ((πΉ:π΄βΆβ β§ π₯ β π΄) β (πΉβπ₯) β β) |
17 | 16 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((πΉ:π΄βΆβ β§ π΄ β dom vol) β§ π₯ β π΄) β (πΉβπ₯) β β) |
18 | 17 | rered 15116 |
. . . . . . . . . . . 12
β’ (((πΉ:π΄βΆβ β§ π΄ β dom vol) β§ π₯ β π΄) β (ββ(πΉβπ₯)) = (πΉβπ₯)) |
19 | 18 | mpteq2dva 5210 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) = (π₯ β π΄ β¦ (πΉβπ₯))) |
20 | 17 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((πΉ:π΄βΆβ β§ π΄ β dom vol) β§ π₯ β π΄) β (πΉβπ₯) β β) |
21 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β πΉ:π΄βΆβ) |
22 | 21 | feqmptd 6915 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
23 | | ref 15004 |
. . . . . . . . . . . . . 14
β’
β:ββΆβ |
24 | 23 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β
β:ββΆβ) |
25 | 24 | feqmptd 6915 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β β = (π¦ β β β¦
(ββπ¦))) |
26 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π¦ = (πΉβπ₯) β (ββπ¦) = (ββ(πΉβπ₯))) |
27 | 20, 22, 25, 26 | fmptco 7080 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β β
πΉ) = (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) |
28 | 19, 27, 22 | 3eqtr4rd 2788 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β πΉ = (β β πΉ)) |
29 | 28 | cnveqd 5836 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β β‘πΉ = β‘(β β πΉ)) |
30 | 29 | imaeq1d 6017 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β‘πΉ β π₯) = (β‘(β β πΉ) β π₯)) |
31 | 30 | eleq1d 2823 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β ((β‘πΉ β π₯) β dom vol β (β‘(β β πΉ) β π₯) β dom vol)) |
32 | | imf 15005 |
. . . . . . . . . . . . . . . 16
β’
β:ββΆβ |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β
β:ββΆβ) |
34 | 33 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β β = (π¦ β β β¦
(ββπ¦))) |
35 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΉβπ₯) β (ββπ¦) = (ββ(πΉβπ₯))) |
36 | 20, 22, 34, 35 | fmptco 7080 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β β
πΉ) = (π₯ β π΄ β¦ (ββ(πΉβπ₯)))) |
37 | 17 | reim0d 15117 |
. . . . . . . . . . . . . 14
β’ (((πΉ:π΄βΆβ β§ π΄ β dom vol) β§ π₯ β π΄) β (ββ(πΉβπ₯)) = 0) |
38 | 37 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (π₯ β π΄ β¦ (ββ(πΉβπ₯))) = (π₯ β π΄ β¦ 0)) |
39 | 36, 38 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β β
πΉ) = (π₯ β π΄ β¦ 0)) |
40 | | fconstmpt 5699 |
. . . . . . . . . . . 12
β’ (π΄ Γ {0}) = (π₯ β π΄ β¦ 0) |
41 | 39, 40 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β β
πΉ) = (π΄ Γ {0})) |
42 | 41 | cnveqd 5836 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β β‘(β β πΉ) = β‘(π΄ Γ {0})) |
43 | 42 | imaeq1d 6017 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β‘(β β πΉ) β π₯) = (β‘(π΄ Γ {0}) β π₯)) |
44 | | simpr 486 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β π΄ β dom vol) |
45 | | 0re 11164 |
. . . . . . . . . 10
β’ 0 β
β |
46 | | mbfconstlem 25007 |
. . . . . . . . . 10
β’ ((π΄ β dom vol β§ 0 β
β) β (β‘(π΄ Γ {0}) β π₯) β dom vol) |
47 | 44, 45, 46 | sylancl 587 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β‘(π΄ Γ {0}) β π₯) β dom vol) |
48 | 43, 47 | eqeltrd 2838 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β‘(β β πΉ) β π₯) β dom vol) |
49 | 48 | biantrud 533 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β ((β‘(β β πΉ) β π₯) β dom vol β ((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
50 | 31, 49 | bitrd 279 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β ((β‘πΉ β π₯) β dom vol β ((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
51 | 50 | ralbidv 3175 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol β βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
52 | | ax-resscn 11115 |
. . . . . . . 8
β’ β
β β |
53 | | fss 6690 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ β β
β) β πΉ:π΄βΆβ) |
54 | 52, 53 | mpan2 690 |
. . . . . . 7
β’ (πΉ:π΄βΆβ β πΉ:π΄βΆβ) |
55 | | mblss 24911 |
. . . . . . 7
β’ (π΄ β dom vol β π΄ β
β) |
56 | | cnex 11139 |
. . . . . . . 8
β’ β
β V |
57 | | reex 11149 |
. . . . . . . 8
β’ β
β V |
58 | | elpm2r 8790 |
. . . . . . . 8
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
59 | 56, 57, 58 | mpanl12 701 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
60 | 54, 55, 59 | syl2an 597 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β πΉ β (β βpm
β)) |
61 | 60 | biantrurd 534 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol) β (πΉ β (β βpm
β) β§ βπ₯
β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol)))) |
62 | 51, 61 | bitrd 279 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol β (πΉ β (β βpm
β) β§ βπ₯
β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol)))) |
63 | 15, 62 | bitr4id 290 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol)) |
64 | 63 | ex 414 |
. 2
β’ (πΉ:π΄βΆβ β (π΄ β dom vol β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol))) |
65 | 4, 14, 64 | pm5.21ndd 381 |
1
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol)) |