Step | Hyp | Ref
| Expression |
1 | | ffvelcdm 7033 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (πΉβπ‘) β β) |
2 | 1 | recnd 11184 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (πΉβπ‘) β β) |
3 | | id 22 |
. . . . 5
β’ (πΉ:π΄βΆβ β πΉ:π΄βΆβ) |
4 | 3 | feqmptd 6911 |
. . . 4
β’ (πΉ:π΄βΆβ β πΉ = (π‘ β π΄ β¦ (πΉβπ‘))) |
5 | | absf 15223 |
. . . . . 6
β’
abs:ββΆβ |
6 | 5 | a1i 11 |
. . . . 5
β’ (πΉ:π΄βΆβ β
abs:ββΆβ) |
7 | 6 | feqmptd 6911 |
. . . 4
β’ (πΉ:π΄βΆβ β abs = (π₯ β β β¦
(absβπ₯))) |
8 | | fveq2 6843 |
. . . 4
β’ (π₯ = (πΉβπ‘) β (absβπ₯) = (absβ(πΉβπ‘))) |
9 | 2, 4, 7, 8 | fmptco 7076 |
. . 3
β’ (πΉ:π΄βΆβ β (abs β πΉ) = (π‘ β π΄ β¦ (absβ(πΉβπ‘)))) |
10 | 9 | adantr 482 |
. 2
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (abs β πΉ) = (π‘ β π΄ β¦ (absβ(πΉβπ‘)))) |
11 | 2 | abscld 15322 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (absβ(πΉβπ‘)) β β) |
12 | 11 | fmpttd 7064 |
. . . 4
β’ (πΉ:π΄βΆβ β (π‘ β π΄ β¦ (absβ(πΉβπ‘))):π΄βΆβ) |
13 | 12 | adantr 482 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (π‘ β π΄ β¦ (absβ(πΉβπ‘))):π΄βΆβ) |
14 | | fdm 6678 |
. . . . 5
β’ (πΉ:π΄βΆβ β dom πΉ = π΄) |
15 | 14 | adantr 482 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β dom πΉ = π΄) |
16 | | mbfdm 24993 |
. . . . 5
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
17 | 16 | adantl 483 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β dom πΉ β dom vol) |
18 | 15, 17 | eqeltrrd 2839 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β π΄ β dom vol) |
19 | | rexr 11202 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯ β
β*) |
20 | | elioopnf 13361 |
. . . . . . . . . . . . 13
β’ (π₯ β β*
β ((absβ(πΉβπ‘)) β (π₯(,)+β) β ((absβ(πΉβπ‘)) β β β§ π₯ < (absβ(πΉβπ‘))))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
β’ (π₯ β β β
((absβ(πΉβπ‘)) β (π₯(,)+β) β ((absβ(πΉβπ‘)) β β β§ π₯ < (absβ(πΉβπ‘))))) |
22 | 11 | biantrurd 534 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (π₯ < (absβ(πΉβπ‘)) β ((absβ(πΉβπ‘)) β β β§ π₯ < (absβ(πΉβπ‘))))) |
23 | 22 | bicomd 222 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (((absβ(πΉβπ‘)) β β β§ π₯ < (absβ(πΉβπ‘))) β π₯ < (absβ(πΉβπ‘)))) |
24 | 21, 23 | sylan9bbr 512 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) β (π₯(,)+β) β π₯ < (absβ(πΉβπ‘)))) |
25 | | ltnle 11235 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§
(absβ(πΉβπ‘)) β β) β (π₯ < (absβ(πΉβπ‘)) β Β¬ (absβ(πΉβπ‘)) β€ π₯)) |
26 | 25 | ancoms 460 |
. . . . . . . . . . . 12
β’
(((absβ(πΉβπ‘)) β β β§ π₯ β β) β (π₯ < (absβ(πΉβπ‘)) β Β¬ (absβ(πΉβπ‘)) β€ π₯)) |
27 | 11, 26 | sylan 581 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (π₯ < (absβ(πΉβπ‘)) β Β¬ (absβ(πΉβπ‘)) β€ π₯)) |
28 | | absle 15201 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ‘) β β β§ π₯ β β) β ((absβ(πΉβπ‘)) β€ π₯ β (-π₯ β€ (πΉβπ‘) β§ (πΉβπ‘) β€ π₯))) |
29 | 1, 28 | sylan 581 |
. . . . . . . . . . . . . 14
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) β€ π₯ β (-π₯ β€ (πΉβπ‘) β§ (πΉβπ‘) β€ π₯))) |
30 | | renegcl 11465 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β -π₯ β
β) |
31 | | lenlt 11234 |
. . . . . . . . . . . . . . . . 17
β’ ((-π₯ β β β§ (πΉβπ‘) β β) β (-π₯ β€ (πΉβπ‘) β Β¬ (πΉβπ‘) < -π₯)) |
32 | 30, 1, 31 | syl2anr 598 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (-π₯ β€ (πΉβπ‘) β Β¬ (πΉβπ‘) < -π₯)) |
33 | 1 | biantrurd 534 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β ((πΉβπ‘) < -π₯ β ((πΉβπ‘) β β β§ (πΉβπ‘) < -π₯))) |
34 | 30 | rexrd 11206 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β -π₯ β
β*) |
35 | | elioomnf 13362 |
. . . . . . . . . . . . . . . . . . . 20
β’ (-π₯ β β*
β ((πΉβπ‘) β (-β(,)-π₯) β ((πΉβπ‘) β β β§ (πΉβπ‘) < -π₯))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β ((πΉβπ‘) β (-β(,)-π₯) β ((πΉβπ‘) β β β§ (πΉβπ‘) < -π₯))) |
37 | 36 | bicomd 222 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (((πΉβπ‘) β β β§ (πΉβπ‘) < -π₯) β (πΉβπ‘) β (-β(,)-π₯))) |
38 | 33, 37 | sylan9bb 511 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((πΉβπ‘) < -π₯ β (πΉβπ‘) β (-β(,)-π₯))) |
39 | 38 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (Β¬ (πΉβπ‘) < -π₯ β Β¬ (πΉβπ‘) β (-β(,)-π₯))) |
40 | 32, 39 | bitrd 279 |
. . . . . . . . . . . . . . 15
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (-π₯ β€ (πΉβπ‘) β Β¬ (πΉβπ‘) β (-β(,)-π₯))) |
41 | | lenlt 11234 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉβπ‘) β β β§ π₯ β β) β ((πΉβπ‘) β€ π₯ β Β¬ π₯ < (πΉβπ‘))) |
42 | 1, 41 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((πΉβπ‘) β€ π₯ β Β¬ π₯ < (πΉβπ‘))) |
43 | 1 | biantrurd 534 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (π₯ < (πΉβπ‘) β ((πΉβπ‘) β β β§ π₯ < (πΉβπ‘)))) |
44 | | elioopnf 13361 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β*
β ((πΉβπ‘) β (π₯(,)+β) β ((πΉβπ‘) β β β§ π₯ < (πΉβπ‘)))) |
45 | 19, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β ((πΉβπ‘) β (π₯(,)+β) β ((πΉβπ‘) β β β§ π₯ < (πΉβπ‘)))) |
46 | 45 | bicomd 222 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (((πΉβπ‘) β β β§ π₯ < (πΉβπ‘)) β (πΉβπ‘) β (π₯(,)+β))) |
47 | 43, 46 | sylan9bb 511 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (π₯ < (πΉβπ‘) β (πΉβπ‘) β (π₯(,)+β))) |
48 | 47 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (Β¬ π₯ < (πΉβπ‘) β Β¬ (πΉβπ‘) β (π₯(,)+β))) |
49 | 42, 48 | bitrd 279 |
. . . . . . . . . . . . . . 15
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((πΉβπ‘) β€ π₯ β Β¬ (πΉβπ‘) β (π₯(,)+β))) |
50 | 40, 49 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((-π₯ β€ (πΉβπ‘) β§ (πΉβπ‘) β€ π₯) β (Β¬ (πΉβπ‘) β (-β(,)-π₯) β§ Β¬ (πΉβπ‘) β (π₯(,)+β)))) |
51 | 29, 50 | bitrd 279 |
. . . . . . . . . . . . 13
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) β€ π₯ β (Β¬ (πΉβπ‘) β (-β(,)-π₯) β§ Β¬ (πΉβπ‘) β (π₯(,)+β)))) |
52 | 51 | notbid 318 |
. . . . . . . . . . . 12
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (Β¬
(absβ(πΉβπ‘)) β€ π₯ β Β¬ (Β¬ (πΉβπ‘) β (-β(,)-π₯) β§ Β¬ (πΉβπ‘) β (π₯(,)+β)))) |
53 | | elun 4109 |
. . . . . . . . . . . . 13
β’ ((πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β)) β ((πΉβπ‘) β (-β(,)-π₯) β¨ (πΉβπ‘) β (π₯(,)+β))) |
54 | | oran 989 |
. . . . . . . . . . . . 13
β’ (((πΉβπ‘) β (-β(,)-π₯) β¨ (πΉβπ‘) β (π₯(,)+β)) β Β¬ (Β¬ (πΉβπ‘) β (-β(,)-π₯) β§ Β¬ (πΉβπ‘) β (π₯(,)+β))) |
55 | 53, 54 | bitri 275 |
. . . . . . . . . . . 12
β’ ((πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β)) β Β¬ (Β¬ (πΉβπ‘) β (-β(,)-π₯) β§ Β¬ (πΉβπ‘) β (π₯(,)+β))) |
56 | 52, 55 | bitr4di 289 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β (Β¬
(absβ(πΉβπ‘)) β€ π₯ β (πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β)))) |
57 | 24, 27, 56 | 3bitrd 305 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) β (π₯(,)+β) β (πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β)))) |
58 | 57 | an32s 651 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ π₯ β β) β§ π‘ β π΄) β ((absβ(πΉβπ‘)) β (π₯(,)+β) β (πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β)))) |
59 | 58 | rabbidva 3415 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β {π‘ β π΄ β£ (absβ(πΉβπ‘)) β (π₯(,)+β)} = {π‘ β π΄ β£ (πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β))}) |
60 | | eqid 2737 |
. . . . . . . . 9
β’ (π‘ β π΄ β¦ (absβ(πΉβπ‘))) = (π‘ β π΄ β¦ (absβ(πΉβπ‘))) |
61 | 60 | mptpreima 6191 |
. . . . . . . 8
β’ (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (π₯(,)+β)) = {π‘ β π΄ β£ (absβ(πΉβπ‘)) β (π₯(,)+β)} |
62 | | eqid 2737 |
. . . . . . . . 9
β’ (π‘ β π΄ β¦ (πΉβπ‘)) = (π‘ β π΄ β¦ (πΉβπ‘)) |
63 | 62 | mptpreima 6191 |
. . . . . . . 8
β’ (β‘(π‘ β π΄ β¦ (πΉβπ‘)) β ((-β(,)-π₯) βͺ (π₯(,)+β))) = {π‘ β π΄ β£ (πΉβπ‘) β ((-β(,)-π₯) βͺ (π₯(,)+β))} |
64 | 59, 61, 63 | 3eqtr4g 2802 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (π₯(,)+β)) = (β‘(π‘ β π΄ β¦ (πΉβπ‘)) β ((-β(,)-π₯) βͺ (π₯(,)+β)))) |
65 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β πΉ:π΄βΆβ) |
66 | 65 | feqmptd 6911 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β πΉ = (π‘ β π΄ β¦ (πΉβπ‘))) |
67 | 66 | cnveqd 5832 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β β‘πΉ = β‘(π‘ β π΄ β¦ (πΉβπ‘))) |
68 | 67 | imaeq1d 6013 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘πΉ β ((-β(,)-π₯) βͺ (π₯(,)+β))) = (β‘(π‘ β π΄ β¦ (πΉβπ‘)) β ((-β(,)-π₯) βͺ (π₯(,)+β)))) |
69 | 64, 68 | eqtr4d 2780 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (π₯(,)+β)) = (β‘πΉ β ((-β(,)-π₯) βͺ (π₯(,)+β)))) |
70 | | imaundi 6103 |
. . . . . 6
β’ (β‘πΉ β ((-β(,)-π₯) βͺ (π₯(,)+β))) = ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β))) |
71 | 69, 70 | eqtrdi 2793 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (π₯(,)+β)) = ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β)))) |
72 | 71 | adantlr 714 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ πΉ β MblFn) β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (π₯(,)+β)) = ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β)))) |
73 | | mbfima 24997 |
. . . . . . 7
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (-β(,)-π₯)) β dom vol) |
74 | | mbfima 24997 |
. . . . . . 7
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
75 | | unmbl 24904 |
. . . . . . 7
β’ (((β‘πΉ β (-β(,)-π₯)) β dom vol β§ (β‘πΉ β (π₯(,)+β)) β dom vol) β ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β))) β dom
vol) |
76 | 73, 74, 75 | syl2anc 585 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β))) β dom
vol) |
77 | 76 | ancoms 460 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β))) β dom
vol) |
78 | 77 | adantr 482 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ πΉ β MblFn) β§ π₯ β β) β ((β‘πΉ β (-β(,)-π₯)) βͺ (β‘πΉ β (π₯(,)+β))) β dom
vol) |
79 | 72, 78 | eqeltrd 2838 |
. . 3
β’ (((πΉ:π΄βΆβ β§ πΉ β MblFn) β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (π₯(,)+β)) β dom
vol) |
80 | | abslt 15200 |
. . . . . . . . . . 11
β’ (((πΉβπ‘) β β β§ π₯ β β) β ((absβ(πΉβπ‘)) < π₯ β (-π₯ < (πΉβπ‘) β§ (πΉβπ‘) < π₯))) |
81 | 1, 80 | sylan 581 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) < π₯ β (-π₯ < (πΉβπ‘) β§ (πΉβπ‘) < π₯))) |
82 | | elioomnf 13362 |
. . . . . . . . . . . 12
β’ (π₯ β β*
β ((absβ(πΉβπ‘)) β (-β(,)π₯) β ((absβ(πΉβπ‘)) β β β§ (absβ(πΉβπ‘)) < π₯))) |
83 | 19, 82 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β β
((absβ(πΉβπ‘)) β (-β(,)π₯) β ((absβ(πΉβπ‘)) β β β§ (absβ(πΉβπ‘)) < π₯))) |
84 | 11 | biantrurd 534 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β ((absβ(πΉβπ‘)) < π₯ β ((absβ(πΉβπ‘)) β β β§ (absβ(πΉβπ‘)) < π₯))) |
85 | 84 | bicomd 222 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (((absβ(πΉβπ‘)) β β β§ (absβ(πΉβπ‘)) < π₯) β (absβ(πΉβπ‘)) < π₯)) |
86 | 83, 85 | sylan9bbr 512 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) β (-β(,)π₯) β (absβ(πΉβπ‘)) < π₯)) |
87 | 34, 19 | jca 513 |
. . . . . . . . . . 11
β’ (π₯ β β β (-π₯ β β*
β§ π₯ β
β*)) |
88 | 1 | rexrd 11206 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (πΉβπ‘) β
β*) |
89 | | elioo5 13322 |
. . . . . . . . . . . 12
β’ ((-π₯ β β*
β§ π₯ β
β* β§ (πΉβπ‘) β β*) β ((πΉβπ‘) β (-π₯(,)π₯) β (-π₯ < (πΉβπ‘) β§ (πΉβπ‘) < π₯))) |
90 | 89 | 3expa 1119 |
. . . . . . . . . . 11
β’ (((-π₯ β β*
β§ π₯ β
β*) β§ (πΉβπ‘) β β*) β ((πΉβπ‘) β (-π₯(,)π₯) β (-π₯ < (πΉβπ‘) β§ (πΉβπ‘) < π₯))) |
91 | 87, 88, 90 | syl2anr 598 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((πΉβπ‘) β (-π₯(,)π₯) β (-π₯ < (πΉβπ‘) β§ (πΉβπ‘) < π₯))) |
92 | 81, 86, 91 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ π‘ β π΄) β§ π₯ β β) β ((absβ(πΉβπ‘)) β (-β(,)π₯) β (πΉβπ‘) β (-π₯(,)π₯))) |
93 | 92 | an32s 651 |
. . . . . . . 8
β’ (((πΉ:π΄βΆβ β§ π₯ β β) β§ π‘ β π΄) β ((absβ(πΉβπ‘)) β (-β(,)π₯) β (πΉβπ‘) β (-π₯(,)π₯))) |
94 | 93 | rabbidva 3415 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β {π‘ β π΄ β£ (absβ(πΉβπ‘)) β (-β(,)π₯)} = {π‘ β π΄ β£ (πΉβπ‘) β (-π₯(,)π₯)}) |
95 | 60 | mptpreima 6191 |
. . . . . . 7
β’ (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (-β(,)π₯)) = {π‘ β π΄ β£ (absβ(πΉβπ‘)) β (-β(,)π₯)} |
96 | 62 | mptpreima 6191 |
. . . . . . 7
β’ (β‘(π‘ β π΄ β¦ (πΉβπ‘)) β (-π₯(,)π₯)) = {π‘ β π΄ β£ (πΉβπ‘) β (-π₯(,)π₯)} |
97 | 94, 95, 96 | 3eqtr4g 2802 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (-β(,)π₯)) = (β‘(π‘ β π΄ β¦ (πΉβπ‘)) β (-π₯(,)π₯))) |
98 | 67 | imaeq1d 6013 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘πΉ β (-π₯(,)π₯)) = (β‘(π‘ β π΄ β¦ (πΉβπ‘)) β (-π₯(,)π₯))) |
99 | 97, 98 | eqtr4d 2780 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (-β(,)π₯)) = (β‘πΉ β (-π₯(,)π₯))) |
100 | 99 | adantlr 714 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ πΉ β MblFn) β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (-β(,)π₯)) = (β‘πΉ β (-π₯(,)π₯))) |
101 | | mbfima 24997 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (-π₯(,)π₯)) β dom vol) |
102 | 101 | ancoms 460 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (β‘πΉ β (-π₯(,)π₯)) β dom vol) |
103 | 102 | adantr 482 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ πΉ β MblFn) β§ π₯ β β) β (β‘πΉ β (-π₯(,)π₯)) β dom vol) |
104 | 100, 103 | eqeltrd 2838 |
. . 3
β’ (((πΉ:π΄βΆβ β§ πΉ β MblFn) β§ π₯ β β) β (β‘(π‘ β π΄ β¦ (absβ(πΉβπ‘))) β (-β(,)π₯)) β dom vol) |
105 | 13, 18, 79, 104 | ismbf2d 25007 |
. 2
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (π‘ β π΄ β¦ (absβ(πΉβπ‘))) β MblFn) |
106 | 10, 105 | eqeltrd 2838 |
1
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (abs β πΉ) β MblFn) |