Step | Hyp | Ref
| Expression |
1 | | ref 15004 |
. . . 4
β’
β:ββΆβ |
2 | | simpr 486 |
. . . . . . 7
β’ ((πΉ β MblFn β§ π΄ β dom vol) β π΄ β dom
vol) |
3 | | ismbf1 25004 |
. . . . . . . . 9
β’ (πΉ β MblFn β (πΉ β (β
βpm β) β§ βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
4 | 3 | simplbi 499 |
. . . . . . . 8
β’ (πΉ β MblFn β πΉ β (β
βpm β)) |
5 | 4 | adantr 482 |
. . . . . . 7
β’ ((πΉ β MblFn β§ π΄ β dom vol) β πΉ β (β
βpm β)) |
6 | | pmresg 8815 |
. . . . . . 7
β’ ((π΄ β dom vol β§ πΉ β (β
βpm β)) β (πΉ βΎ π΄) β (β βpm π΄)) |
7 | 2, 5, 6 | syl2anc 585 |
. . . . . 6
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (πΉ βΎ π΄) β (β βpm π΄)) |
8 | | cnex 11139 |
. . . . . . 7
β’ β
β V |
9 | | elpm2g 8789 |
. . . . . . 7
β’ ((β
β V β§ π΄ β dom
vol) β ((πΉ βΎ
π΄) β (β
βpm π΄)
β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β§ dom (πΉ βΎ π΄) β π΄))) |
10 | 8, 2, 9 | sylancr 588 |
. . . . . 6
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((πΉ βΎ π΄) β (β βpm π΄) β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β§ dom (πΉ βΎ π΄) β π΄))) |
11 | 7, 10 | mpbid 231 |
. . . . 5
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β§ dom (πΉ βΎ π΄) β π΄)) |
12 | 11 | simpld 496 |
. . . 4
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ) |
13 | | fco 6697 |
. . . 4
β’
((β:ββΆβ β§ (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ) β (β β
(πΉ βΎ π΄)):dom (πΉ βΎ π΄)βΆβ) |
14 | 1, 12, 13 | sylancr 588 |
. . 3
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β
β (πΉ βΎ π΄)):dom (πΉ βΎ π΄)βΆβ) |
15 | | dmres 5964 |
. . . 4
β’ dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) |
16 | | id 22 |
. . . . 5
β’ (π΄ β dom vol β π΄ β dom
vol) |
17 | | mbfdm 25006 |
. . . . 5
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
18 | | inmbl 24922 |
. . . . 5
β’ ((π΄ β dom vol β§ dom πΉ β dom vol) β (π΄ β© dom πΉ) β dom vol) |
19 | 16, 17, 18 | syl2anr 598 |
. . . 4
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (π΄ β© dom πΉ) β dom vol) |
20 | 15, 19 | eqeltrid 2842 |
. . 3
β’ ((πΉ β MblFn β§ π΄ β dom vol) β dom
(πΉ βΎ π΄) β dom
vol) |
21 | | resco 6207 |
. . . . . . . 8
β’ ((β
β πΉ) βΎ π΄) = (β β (πΉ βΎ π΄)) |
22 | 21 | cnveqi 5835 |
. . . . . . 7
β’ β‘((β β πΉ) βΎ π΄) = β‘(β β (πΉ βΎ π΄)) |
23 | 22 | imaeq1i 6015 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (π₯(,)+β)) = (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) |
24 | | cnvresima 6187 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (π₯(,)+β)) = ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) |
25 | 23, 24 | eqtr3i 2767 |
. . . . 5
β’ (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) = ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) |
26 | | mbff 25005 |
. . . . . . . . . 10
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) |
27 | | ismbfcn 25009 |
. . . . . . . . . 10
β’ (πΉ:dom πΉβΆβ β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn))) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
β’ (πΉ β MblFn β (πΉ β MblFn β ((β
β πΉ) β MblFn
β§ (β β πΉ)
β MblFn))) |
29 | 28 | ibi 267 |
. . . . . . . 8
β’ (πΉ β MblFn β ((β
β πΉ) β MblFn
β§ (β β πΉ)
β MblFn)) |
30 | 29 | simpld 496 |
. . . . . . 7
β’ (πΉ β MblFn β (β
β πΉ) β
MblFn) |
31 | | fco 6697 |
. . . . . . . 8
β’
((β:ββΆβ β§ πΉ:dom πΉβΆβ) β (β β
πΉ):dom πΉβΆβ) |
32 | 1, 26, 31 | sylancr 588 |
. . . . . . 7
β’ (πΉ β MblFn β (β
β πΉ):dom πΉβΆβ) |
33 | | mbfima 25010 |
. . . . . . 7
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ):dom πΉβΆβ) β (β‘(β β πΉ) β (π₯(,)+β)) β dom
vol) |
34 | 30, 32, 33 | syl2anc 585 |
. . . . . 6
β’ (πΉ β MblFn β (β‘(β β πΉ) β (π₯(,)+β)) β dom
vol) |
35 | | inmbl 24922 |
. . . . . 6
β’ (((β‘(β β πΉ) β (π₯(,)+β)) β dom vol β§ π΄ β dom vol) β ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) β dom vol) |
36 | 34, 35 | sylan 581 |
. . . . 5
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) β dom vol) |
37 | 25, 36 | eqeltrid 2842 |
. . . 4
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) β dom
vol) |
38 | 37 | adantr 482 |
. . 3
β’ (((πΉ β MblFn β§ π΄ β dom vol) β§ π₯ β β) β (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) β dom
vol) |
39 | 22 | imaeq1i 6015 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (-β(,)π₯)) = (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) |
40 | | cnvresima 6187 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (-β(,)π₯)) = ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) |
41 | 39, 40 | eqtr3i 2767 |
. . . . 5
β’ (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) = ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) |
42 | | mbfima 25010 |
. . . . . . 7
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ):dom πΉβΆβ) β (β‘(β β πΉ) β (-β(,)π₯)) β dom vol) |
43 | 30, 32, 42 | syl2anc 585 |
. . . . . 6
β’ (πΉ β MblFn β (β‘(β β πΉ) β (-β(,)π₯)) β dom vol) |
44 | | inmbl 24922 |
. . . . . 6
β’ (((β‘(β β πΉ) β (-β(,)π₯)) β dom vol β§ π΄ β dom vol) β ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) β dom vol) |
45 | 43, 44 | sylan 581 |
. . . . 5
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) β dom vol) |
46 | 41, 45 | eqeltrid 2842 |
. . . 4
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) β dom vol) |
47 | 46 | adantr 482 |
. . 3
β’ (((πΉ β MblFn β§ π΄ β dom vol) β§ π₯ β β) β (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) β dom vol) |
48 | 14, 20, 38, 47 | ismbf2d 25020 |
. 2
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β
β (πΉ βΎ π΄)) β
MblFn) |
49 | | imf 15005 |
. . . 4
β’
β:ββΆβ |
50 | | fco 6697 |
. . . 4
β’
((β:ββΆβ β§ (πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ) β (β β
(πΉ βΎ π΄)):dom (πΉ βΎ π΄)βΆβ) |
51 | 49, 12, 50 | sylancr 588 |
. . 3
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β
β (πΉ βΎ π΄)):dom (πΉ βΎ π΄)βΆβ) |
52 | | resco 6207 |
. . . . . . . 8
β’ ((β
β πΉ) βΎ π΄) = (β β (πΉ βΎ π΄)) |
53 | 52 | cnveqi 5835 |
. . . . . . 7
β’ β‘((β β πΉ) βΎ π΄) = β‘(β β (πΉ βΎ π΄)) |
54 | 53 | imaeq1i 6015 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (π₯(,)+β)) = (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) |
55 | | cnvresima 6187 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (π₯(,)+β)) = ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) |
56 | 54, 55 | eqtr3i 2767 |
. . . . 5
β’ (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) = ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) |
57 | 29 | simprd 497 |
. . . . . . 7
β’ (πΉ β MblFn β (β
β πΉ) β
MblFn) |
58 | | fco 6697 |
. . . . . . . 8
β’
((β:ββΆβ β§ πΉ:dom πΉβΆβ) β (β β
πΉ):dom πΉβΆβ) |
59 | 49, 26, 58 | sylancr 588 |
. . . . . . 7
β’ (πΉ β MblFn β (β
β πΉ):dom πΉβΆβ) |
60 | | mbfima 25010 |
. . . . . . 7
β’
(((β β πΉ) β MblFn β§ (β β πΉ):dom πΉβΆβ) β (β‘(β β πΉ) β (π₯(,)+β)) β dom
vol) |
61 | 57, 59, 60 | syl2anc 585 |
. . . . . 6
β’ (πΉ β MblFn β (β‘(β β πΉ) β (π₯(,)+β)) β dom
vol) |
62 | | inmbl 24922 |
. . . . . 6
β’ (((β‘(β β πΉ) β (π₯(,)+β)) β dom vol β§ π΄ β dom vol) β ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) β dom vol) |
63 | 61, 62 | sylan 581 |
. . . . 5
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((β‘(β β πΉ) β (π₯(,)+β)) β© π΄) β dom vol) |
64 | 56, 63 | eqeltrid 2842 |
. . . 4
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) β dom
vol) |
65 | 64 | adantr 482 |
. . 3
β’ (((πΉ β MblFn β§ π΄ β dom vol) β§ π₯ β β) β (β‘(β β (πΉ βΎ π΄)) β (π₯(,)+β)) β dom
vol) |
66 | 53 | imaeq1i 6015 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (-β(,)π₯)) = (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) |
67 | | cnvresima 6187 |
. . . . . 6
β’ (β‘((β β πΉ) βΎ π΄) β (-β(,)π₯)) = ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) |
68 | 66, 67 | eqtr3i 2767 |
. . . . 5
β’ (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) = ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) |
69 | | mbfima 25010 |
. . . . . . 7
β’
(((β β πΉ) β MblFn β§ (β β πΉ):dom πΉβΆβ) β (β‘(β β πΉ) β (-β(,)π₯)) β dom vol) |
70 | 57, 59, 69 | syl2anc 585 |
. . . . . 6
β’ (πΉ β MblFn β (β‘(β β πΉ) β (-β(,)π₯)) β dom vol) |
71 | | inmbl 24922 |
. . . . . 6
β’ (((β‘(β β πΉ) β (-β(,)π₯)) β dom vol β§ π΄ β dom vol) β ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) β dom vol) |
72 | 70, 71 | sylan 581 |
. . . . 5
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((β‘(β β πΉ) β (-β(,)π₯)) β© π΄) β dom vol) |
73 | 68, 72 | eqeltrid 2842 |
. . . 4
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) β dom vol) |
74 | 73 | adantr 482 |
. . 3
β’ (((πΉ β MblFn β§ π΄ β dom vol) β§ π₯ β β) β (β‘(β β (πΉ βΎ π΄)) β (-β(,)π₯)) β dom vol) |
75 | 51, 20, 65, 74 | ismbf2d 25020 |
. 2
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (β
β (πΉ βΎ π΄)) β
MblFn) |
76 | | ismbfcn 25009 |
. . 3
β’ ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β ((πΉ βΎ π΄) β MblFn β ((β β
(πΉ βΎ π΄)) β MblFn β§ (β
β (πΉ βΎ π΄)) β
MblFn))) |
77 | 12, 76 | syl 17 |
. 2
β’ ((πΉ β MblFn β§ π΄ β dom vol) β ((πΉ βΎ π΄) β MblFn β ((β β
(πΉ βΎ π΄)) β MblFn β§ (β
β (πΉ βΎ π΄)) β
MblFn))) |
78 | 48, 75, 77 | mpbir2and 712 |
1
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (πΉ βΎ π΄) β MblFn) |