Step | Hyp | Ref
| Expression |
1 | | ismbf2d.1 |
. 2
β’ (π β πΉ:π΄βΆβ) |
2 | | elxr 13044 |
. . 3
β’ (π₯ β β*
β (π₯ β β
β¨ π₯ = +β β¨
π₯ =
-β)) |
3 | | ismbf2d.3 |
. . . 4
β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
4 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = +β β (π₯(,)+β) =
(+β(,)+β)) |
5 | | iooid 13299 |
. . . . . . . 8
β’
(+β(,)+β) = β
|
6 | 4, 5 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = +β β (π₯(,)+β) =
β
) |
7 | 6 | imaeq2d 6018 |
. . . . . 6
β’ (π₯ = +β β (β‘πΉ β (π₯(,)+β)) = (β‘πΉ β β
)) |
8 | | ima0 6034 |
. . . . . . 7
β’ (β‘πΉ β β
) = β
|
9 | | 0mbl 24919 |
. . . . . . 7
β’ β
β dom vol |
10 | 8, 9 | eqeltri 2834 |
. . . . . 6
β’ (β‘πΉ β β
) β dom
vol |
11 | 7, 10 | eqeltrdi 2846 |
. . . . 5
β’ (π₯ = +β β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
12 | 11 | adantl 483 |
. . . 4
β’ ((π β§ π₯ = +β) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
13 | | fimacnv 6695 |
. . . . . . . 8
β’ (πΉ:π΄βΆβ β (β‘πΉ β β) = π΄) |
14 | 1, 13 | syl 17 |
. . . . . . 7
β’ (π β (β‘πΉ β β) = π΄) |
15 | | ismbf2d.2 |
. . . . . . 7
β’ (π β π΄ β dom vol) |
16 | 14, 15 | eqeltrd 2838 |
. . . . . 6
β’ (π β (β‘πΉ β β) β dom
vol) |
17 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = -β β (π₯(,)+β) =
(-β(,)+β)) |
18 | | ioomax 13346 |
. . . . . . . . 9
β’
(-β(,)+β) = β |
19 | 17, 18 | eqtrdi 2793 |
. . . . . . . 8
β’ (π₯ = -β β (π₯(,)+β) =
β) |
20 | 19 | imaeq2d 6018 |
. . . . . . 7
β’ (π₯ = -β β (β‘πΉ β (π₯(,)+β)) = (β‘πΉ β β)) |
21 | 20 | eleq1d 2823 |
. . . . . 6
β’ (π₯ = -β β ((β‘πΉ β (π₯(,)+β)) β dom vol β (β‘πΉ β β) β dom
vol)) |
22 | 16, 21 | syl5ibrcom 247 |
. . . . 5
β’ (π β (π₯ = -β β (β‘πΉ β (π₯(,)+β)) β dom
vol)) |
23 | 22 | imp 408 |
. . . 4
β’ ((π β§ π₯ = -β) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
24 | 3, 12, 23 | 3jaodan 1431 |
. . 3
β’ ((π β§ (π₯ β β β¨ π₯ = +β β¨ π₯ = -β)) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
25 | 2, 24 | sylan2b 595 |
. 2
β’ ((π β§ π₯ β β*) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
26 | | ismbf2d.4 |
. . . 4
β’ ((π β§ π₯ β β) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
27 | | oveq2 7370 |
. . . . . . . . 9
β’ (π₯ = +β β
(-β(,)π₯) =
(-β(,)+β)) |
28 | 27, 18 | eqtrdi 2793 |
. . . . . . . 8
β’ (π₯ = +β β
(-β(,)π₯) =
β) |
29 | 28 | imaeq2d 6018 |
. . . . . . 7
β’ (π₯ = +β β (β‘πΉ β (-β(,)π₯)) = (β‘πΉ β β)) |
30 | 29 | eleq1d 2823 |
. . . . . 6
β’ (π₯ = +β β ((β‘πΉ β (-β(,)π₯)) β dom vol β (β‘πΉ β β) β dom
vol)) |
31 | 16, 30 | syl5ibrcom 247 |
. . . . 5
β’ (π β (π₯ = +β β (β‘πΉ β (-β(,)π₯)) β dom vol)) |
32 | 31 | imp 408 |
. . . 4
β’ ((π β§ π₯ = +β) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
33 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = -β β
(-β(,)π₯) =
(-β(,)-β)) |
34 | | iooid 13299 |
. . . . . . . 8
β’
(-β(,)-β) = β
|
35 | 33, 34 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = -β β
(-β(,)π₯) =
β
) |
36 | 35 | imaeq2d 6018 |
. . . . . 6
β’ (π₯ = -β β (β‘πΉ β (-β(,)π₯)) = (β‘πΉ β β
)) |
37 | 36, 10 | eqeltrdi 2846 |
. . . . 5
β’ (π₯ = -β β (β‘πΉ β (-β(,)π₯)) β dom vol) |
38 | 37 | adantl 483 |
. . . 4
β’ ((π β§ π₯ = -β) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
39 | 26, 32, 38 | 3jaodan 1431 |
. . 3
β’ ((π β§ (π₯ β β β¨ π₯ = +β β¨ π₯ = -β)) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
40 | 2, 39 | sylan2b 595 |
. 2
β’ ((π β§ π₯ β β*) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
41 | 1, 25, 40 | ismbfd 25019 |
1
β’ (π β πΉ β MblFn) |