Step | Hyp | Ref
| Expression |
1 | | ioof 13371 |
. . . . 5
β’
(,):(β* Γ β*)βΆπ«
β |
2 | | ffn 6673 |
. . . . 5
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
3 | | ovelrn 7535 |
. . . . 5
β’ ((,) Fn
(β* Γ β*) β (π§ β ran (,) β βπ₯ β β*
βπ¦ β
β* π§ =
(π₯(,)π¦))) |
4 | 1, 2, 3 | mp2b 10 |
. . . 4
β’ (π§ β ran (,) β
βπ₯ β
β* βπ¦ β β* π§ = (π₯(,)π¦)) |
5 | | simprl 770 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β π₯ β
β*) |
6 | | pnfxr 11216 |
. . . . . . . . . . . 12
β’ +β
β β* |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β +β β β*) |
8 | | mnfxr 11219 |
. . . . . . . . . . . 12
β’ -β
β β* |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β -β β β*) |
10 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β π¦ β
β*) |
11 | | iooin 13305 |
. . . . . . . . . . 11
β’ (((π₯ β β*
β§ +β β β*) β§ (-β β
β* β§ π¦
β β*)) β ((π₯(,)+β) β© (-β(,)π¦)) = (if(π₯ β€ -β, -β, π₯)(,)if(+β β€ π¦, +β, π¦))) |
12 | 5, 7, 9, 10, 11 | syl22anc 838 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β ((π₯(,)+β)
β© (-β(,)π¦)) =
(if(π₯ β€ -β,
-β, π₯)(,)if(+β
β€ π¦, +β, π¦))) |
13 | | ifcl 4536 |
. . . . . . . . . . . . 13
β’
((-β β β* β§ π₯ β β*) β if(π₯ β€ -β, -β, π₯) β
β*) |
14 | 8, 5, 13 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β if(π₯ β€ -β,
-β, π₯) β
β*) |
15 | | mnfle 13062 |
. . . . . . . . . . . . . 14
β’ (π₯ β β*
β -β β€ π₯) |
16 | | xrleid 13077 |
. . . . . . . . . . . . . 14
β’ (π₯ β β*
β π₯ β€ π₯) |
17 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (-β
= if(π₯ β€ -β,
-β, π₯) β
(-β β€ π₯ β
if(π₯ β€ -β,
-β, π₯) β€ π₯)) |
18 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π₯ = if(π₯ β€ -β, -β, π₯) β (π₯ β€ π₯ β if(π₯ β€ -β, -β, π₯) β€ π₯)) |
19 | 17, 18 | ifboth 4530 |
. . . . . . . . . . . . . 14
β’
((-β β€ π₯
β§ π₯ β€ π₯) β if(π₯ β€ -β, -β, π₯) β€ π₯) |
20 | 15, 16, 19 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π₯ β β*
β if(π₯ β€ -β,
-β, π₯) β€ π₯) |
21 | 20 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β if(π₯ β€ -β,
-β, π₯) β€ π₯) |
22 | | xrmax1 13101 |
. . . . . . . . . . . . 13
β’ ((π₯ β β*
β§ -β β β*) β π₯ β€ if(π₯ β€ -β, -β, π₯)) |
23 | 5, 8, 22 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β π₯ β€ if(π₯ β€ -β, -β, π₯)) |
24 | 14, 5, 21, 23 | xrletrid 13081 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β if(π₯ β€ -β,
-β, π₯) = π₯) |
25 | | ifcl 4536 |
. . . . . . . . . . . . 13
β’
((+β β β* β§ π¦ β β*) β
if(+β β€ π¦,
+β, π¦) β
β*) |
26 | 6, 10, 25 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β if(+β β€ π¦,
+β, π¦) β
β*) |
27 | | xrmin2 13104 |
. . . . . . . . . . . . 13
β’
((+β β β* β§ π¦ β β*) β
if(+β β€ π¦,
+β, π¦) β€ π¦) |
28 | 6, 10, 27 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β if(+β β€ π¦,
+β, π¦) β€ π¦) |
29 | | pnfge 13058 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β π¦ β€
+β) |
30 | | xrleid 13077 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β π¦ β€ π¦) |
31 | | breq2 5114 |
. . . . . . . . . . . . . . 15
β’ (+β
= if(+β β€ π¦,
+β, π¦) β (π¦ β€ +β β π¦ β€ if(+β β€ π¦, +β, π¦))) |
32 | | breq2 5114 |
. . . . . . . . . . . . . . 15
β’ (π¦ = if(+β β€ π¦, +β, π¦) β (π¦ β€ π¦ β π¦ β€ if(+β β€ π¦, +β, π¦))) |
33 | 31, 32 | ifboth 4530 |
. . . . . . . . . . . . . 14
β’ ((π¦ β€ +β β§ π¦ β€ π¦) β π¦ β€ if(+β β€ π¦, +β, π¦)) |
34 | 29, 30, 33 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π¦ β β*
β π¦ β€ if(+β
β€ π¦, +β, π¦)) |
35 | 34 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β π¦ β€ if(+β
β€ π¦, +β, π¦)) |
36 | 26, 10, 28, 35 | xrletrid 13081 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β if(+β β€ π¦,
+β, π¦) = π¦) |
37 | 24, 36 | oveq12d 7380 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (if(π₯ β€ -β,
-β, π₯)(,)if(+β
β€ π¦, +β, π¦)) = (π₯(,)π¦)) |
38 | 12, 37 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β ((π₯(,)+β)
β© (-β(,)π¦)) =
(π₯(,)π¦)) |
39 | 38 | imaeq2d 6018 |
. . . . . . . 8
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (β‘πΉ β ((π₯(,)+β) β© (-β(,)π¦))) = (β‘πΉ β (π₯(,)π¦))) |
40 | | ismbfd.1 |
. . . . . . . . . . 11
β’ (π β πΉ:π΄βΆβ) |
41 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β πΉ:π΄βΆβ) |
42 | 41 | ffund 6677 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β Fun πΉ) |
43 | | inpreima 7019 |
. . . . . . . . 9
β’ (Fun
πΉ β (β‘πΉ β ((π₯(,)+β) β© (-β(,)π¦))) = ((β‘πΉ β (π₯(,)+β)) β© (β‘πΉ β (-β(,)π¦)))) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (β‘πΉ β ((π₯(,)+β) β© (-β(,)π¦))) = ((β‘πΉ β (π₯(,)+β)) β© (β‘πΉ β (-β(,)π¦)))) |
45 | 39, 44 | eqtr3d 2779 |
. . . . . . 7
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (β‘πΉ β (π₯(,)π¦)) = ((β‘πΉ β (π₯(,)+β)) β© (β‘πΉ β (-β(,)π¦)))) |
46 | | ismbfd.2 |
. . . . . . . . 9
β’ ((π β§ π₯ β β*) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
47 | 46 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
48 | | ismbfd.3 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β*) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
49 | 48 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ₯ β β* (β‘πΉ β (-β(,)π₯)) β dom vol) |
50 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (-β(,)π₯) = (-β(,)π¦)) |
51 | 50 | imaeq2d 6018 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (β‘πΉ β (-β(,)π₯)) = (β‘πΉ β (-β(,)π¦))) |
52 | 51 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β ((β‘πΉ β (-β(,)π₯)) β dom vol β (β‘πΉ β (-β(,)π¦)) β dom vol)) |
53 | 52 | rspccva 3583 |
. . . . . . . . . 10
β’
((βπ₯ β
β* (β‘πΉ β (-β(,)π₯)) β dom vol β§ π¦ β β*) β (β‘πΉ β (-β(,)π¦)) β dom vol) |
54 | 49, 53 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π¦ β β*) β (β‘πΉ β (-β(,)π¦)) β dom vol) |
55 | 54 | adantrl 715 |
. . . . . . . 8
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (β‘πΉ β (-β(,)π¦)) β dom vol) |
56 | | inmbl 24922 |
. . . . . . . 8
β’ (((β‘πΉ β (π₯(,)+β)) β dom vol β§ (β‘πΉ β (-β(,)π¦)) β dom vol) β ((β‘πΉ β (π₯(,)+β)) β© (β‘πΉ β (-β(,)π¦))) β dom vol) |
57 | 47, 55, 56 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β ((β‘πΉ β (π₯(,)+β)) β© (β‘πΉ β (-β(,)π¦))) β dom vol) |
58 | 45, 57 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (β‘πΉ β (π₯(,)π¦)) β dom vol) |
59 | | imaeq2 6014 |
. . . . . . 7
β’ (π§ = (π₯(,)π¦) β (β‘πΉ β π§) = (β‘πΉ β (π₯(,)π¦))) |
60 | 59 | eleq1d 2823 |
. . . . . 6
β’ (π§ = (π₯(,)π¦) β ((β‘πΉ β π§) β dom vol β (β‘πΉ β (π₯(,)π¦)) β dom vol)) |
61 | 58, 60 | syl5ibrcom 247 |
. . . . 5
β’ ((π β§ (π₯ β β* β§ π¦ β β*))
β (π§ = (π₯(,)π¦) β (β‘πΉ β π§) β dom vol)) |
62 | 61 | rexlimdvva 3206 |
. . . 4
β’ (π β (βπ₯ β β* βπ¦ β β*
π§ = (π₯(,)π¦) β (β‘πΉ β π§) β dom vol)) |
63 | 4, 62 | biimtrid 241 |
. . 3
β’ (π β (π§ β ran (,) β (β‘πΉ β π§) β dom vol)) |
64 | 63 | ralrimiv 3143 |
. 2
β’ (π β βπ§ β ran (,)(β‘πΉ β π§) β dom vol) |
65 | | ismbf 25008 |
. . 3
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β βπ§ β ran (,)(β‘πΉ β π§) β dom vol)) |
66 | 40, 65 | syl 17 |
. 2
β’ (π β (πΉ β MblFn β βπ§ β ran (,)(β‘πΉ β π§) β dom vol)) |
67 | 64, 66 | mpbird 257 |
1
β’ (π β πΉ β MblFn) |