Step | Hyp | Ref
| Expression |
1 | | elpri 4613 |
. . 3
β’ (πΊ β {β, β} β
(πΊ = β β¨ πΊ = β)) |
2 | | fveq1 6846 |
. . . . . . . . . 10
β’ (πΊ = β β (πΊβ(πΉβπ‘)) = (ββ(πΉβπ‘))) |
3 | 2 | fveq2d 6851 |
. . . . . . . . 9
β’ (πΊ = β β
(absβ(πΊβ(πΉβπ‘))) = (absβ(ββ(πΉβπ‘)))) |
4 | 3 | ifeq1d 4510 |
. . . . . . . 8
β’ (πΊ = β β if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0) = if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0)) |
5 | 4 | mpteq2dv 5212 |
. . . . . . 7
β’ (πΊ = β β (π‘ β β β¦ if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0)) = (π‘ β β β¦ if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0))) |
6 | 5 | fveq2d 6851 |
. . . . . 6
β’ (πΊ = β β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) = (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0)))) |
7 | 6 | adantl 483 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ = β) β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) = (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0)))) |
8 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (πΉβπ‘) β β) |
9 | 8 | recld 15086 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (ββ(πΉβπ‘)) β β) |
10 | 9 | adantlr 714 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ π‘ β π΄) β (ββ(πΉβπ‘)) β β) |
11 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β πΉ:π΄βΆβ) |
12 | 11 | feqmptd 6915 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β πΉ = (π‘ β π΄ β¦ (πΉβπ‘))) |
13 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β πΉ β
πΏ1) |
14 | 12, 13 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (πΉβπ‘)) β
πΏ1) |
15 | 8 | iblcn 25179 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ β ((π‘ β π΄ β¦ (πΉβπ‘)) β πΏ1 β
((π‘ β π΄ β¦ (ββ(πΉβπ‘))) β πΏ1 β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β
πΏ1))) |
16 | 15 | biimpa 478 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ (π‘ β π΄ β¦ (πΉβπ‘)) β πΏ1) β
((π‘ β π΄ β¦ (ββ(πΉβπ‘))) β πΏ1 β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β
πΏ1)) |
17 | 14, 16 | syldan 592 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
((π‘ β π΄ β¦ (ββ(πΉβπ‘))) β πΏ1 β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β
πΏ1)) |
18 | 17 | simpld 496 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β
πΏ1) |
19 | 9 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (ββ(πΉβπ‘)) β β) |
20 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ β (π‘ β π΄ β¦ (ββ(πΉβπ‘))) = (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) |
21 | | absf 15229 |
. . . . . . . . . . . . . 14
β’
abs:ββΆβ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . 13
β’ (πΉ:π΄βΆβ β
abs:ββΆβ) |
23 | 22 | feqmptd 6915 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ β abs = (π₯ β β β¦
(absβπ₯))) |
24 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = (ββ(πΉβπ‘)) β (absβπ₯) = (absβ(ββ(πΉβπ‘)))) |
25 | 19, 20, 23, 24 | fmptco 7080 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆβ β (abs β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) = (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘))))) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (abs
β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) = (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘))))) |
27 | 9 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ β (π‘ β π΄ β¦ (ββ(πΉβπ‘))):π΄βΆβ) |
28 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (ββ(πΉβπ‘))):π΄βΆβ) |
29 | | iblmbf 25148 |
. . . . . . . . . . . . . . 15
β’ (πΉ β πΏ1
β πΉ β
MblFn) |
30 | 29 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β πΉ β MblFn) |
31 | 12, 30 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (πΉβπ‘)) β MblFn) |
32 | 8 | ismbfcn2 25018 |
. . . . . . . . . . . . . 14
β’ (πΉ:π΄βΆβ β ((π‘ β π΄ β¦ (πΉβπ‘)) β MblFn β ((π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn))) |
33 | 32 | biimpa 478 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ (π‘ β π΄ β¦ (πΉβπ‘)) β MblFn) β ((π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn)) |
34 | 31, 33 | syldan 592 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
((π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn)) |
35 | 34 | simpld 496 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn) |
36 | | ftc1anclem1 36180 |
. . . . . . . . . . 11
β’ (((π‘ β π΄ β¦ (ββ(πΉβπ‘))):π΄βΆβ β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn) β (abs β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) β MblFn) |
37 | 28, 35, 36 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (abs
β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) β MblFn) |
38 | 26, 37 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘)))) β MblFn) |
39 | 10, 18, 38 | iblabsnc 36171 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘)))) β
πΏ1) |
40 | 19 | abscld 15328 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (absβ(ββ(πΉβπ‘))) β β) |
41 | 19 | absge0d 15336 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β 0 β€
(absβ(ββ(πΉβπ‘)))) |
42 | 40, 41 | iblpos 25173 |
. . . . . . . . 9
β’ (πΉ:π΄βΆβ β ((π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘)))) β πΏ1 β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β))) |
43 | 42 | adantr 482 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β πΏ1 β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β))) |
44 | 39, 43 | mpbid 231 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β)) |
45 | 44 | simprd 497 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
46 | 45 | adantr 482 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ = β) β
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
47 | 7, 46 | eqeltrd 2838 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ = β) β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) β β) |
48 | | fveq1 6846 |
. . . . . . . . . 10
β’ (πΊ = β β (πΊβ(πΉβπ‘)) = (ββ(πΉβπ‘))) |
49 | 48 | fveq2d 6851 |
. . . . . . . . 9
β’ (πΊ = β β
(absβ(πΊβ(πΉβπ‘))) = (absβ(ββ(πΉβπ‘)))) |
50 | 49 | ifeq1d 4510 |
. . . . . . . 8
β’ (πΊ = β β if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0) = if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0)) |
51 | 50 | mpteq2dv 5212 |
. . . . . . 7
β’ (πΊ = β β (π‘ β β β¦ if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0)) = (π‘ β β β¦ if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0))) |
52 | 51 | fveq2d 6851 |
. . . . . 6
β’ (πΊ = β β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) = (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0)))) |
53 | 52 | adantl 483 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ = β) β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) = (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(ββ(πΉβπ‘))), 0)))) |
54 | 8 | imcld 15087 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (ββ(πΉβπ‘)) β β) |
55 | 54 | recnd 11190 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (ββ(πΉβπ‘)) β β) |
56 | 55 | adantlr 714 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ π‘ β π΄) β (ββ(πΉβπ‘)) β β) |
57 | 17 | simprd 497 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β
πΏ1) |
58 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ β (π‘ β π΄ β¦ (ββ(πΉβπ‘))) = (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) |
59 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π₯ = (ββ(πΉβπ‘)) β (absβπ₯) = (absβ(ββ(πΉβπ‘)))) |
60 | 55, 58, 23, 59 | fmptco 7080 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆβ β (abs β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) = (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘))))) |
61 | 60 | adantr 482 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (abs
β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) = (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘))))) |
62 | 54 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆβ β (π‘ β π΄ β¦ (ββ(πΉβπ‘))):π΄βΆβ) |
63 | 62 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (ββ(πΉβπ‘))):π΄βΆβ) |
64 | 34 | simprd 497 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn) |
65 | | ftc1anclem1 36180 |
. . . . . . . . . . 11
β’ (((π‘ β π΄ β¦ (ββ(πΉβπ‘))):π΄βΆβ β§ (π‘ β π΄ β¦ (ββ(πΉβπ‘))) β MblFn) β (abs β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) β MblFn) |
66 | 63, 64, 65 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (abs
β (π‘ β π΄ β¦ (ββ(πΉβπ‘)))) β MblFn) |
67 | 61, 66 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘)))) β MblFn) |
68 | 56, 57, 67 | iblabsnc 36171 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β (π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘)))) β
πΏ1) |
69 | 55 | abscld 15328 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β (absβ(ββ(πΉβπ‘))) β β) |
70 | 55 | absge0d 15336 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π‘ β π΄) β 0 β€
(absβ(ββ(πΉβπ‘)))) |
71 | 69, 70 | iblpos 25173 |
. . . . . . . . 9
β’ (πΉ:π΄βΆβ β ((π‘ β π΄ β¦ (absβ(ββ(πΉβπ‘)))) β πΏ1 β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β))) |
72 | 71 | adantr 482 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β πΏ1 β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β))) |
73 | 68, 72 | mpbid 231 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
((π‘ β π΄ β¦
(absβ(ββ(πΉβπ‘)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β)) |
74 | 73 | simprd 497 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1) β
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
75 | 74 | adantr 482 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ = β) β
(β«2β(π‘
β β β¦ if(π‘
β π΄,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
76 | 53, 75 | eqeltrd 2838 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ = β) β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) β β) |
77 | 47, 76 | jaodan 957 |
. . 3
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ (πΊ = β β¨ πΊ = β)) β
(β«2β(π‘
β β β¦ if(π‘
β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) β β) |
78 | 1, 77 | sylan2 594 |
. 2
β’ (((πΉ:π΄βΆβ β§ πΉ β πΏ1) β§ πΊ β {β, β})
β (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) β β) |
79 | 78 | 3impa 1111 |
1
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1 β§ πΊ β {β, β})
β (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) β β) |