Step | Hyp | Ref
| Expression |
1 | | iblmbf 25155 |
. . 3
β’ ((π₯ β π΄ β¦ π΅) β πΏ1 β (π₯ β π΄ β¦ π΅) β MblFn) |
2 | 1 | a1i 11 |
. 2
β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β (π₯ β π΄ β¦ π΅) β MblFn)) |
3 | | simp1 1137 |
. . 3
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π
β β β§ π β β) β§ (π β β β§ π β β)) β (π₯ β π΄ β¦ π΅) β MblFn) |
4 | 3 | a1i 11 |
. 2
β’ (π β (((π₯ β π΄ β¦ π΅) β MblFn β§ (π
β β β§ π β β) β§ (π β β β§ π β β)) β (π₯ β π΄ β¦ π΅) β MblFn)) |
5 | | eqid 2733 |
. . . . . 6
β’
(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) |
6 | | eqid 2733 |
. . . . . 6
β’
(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) |
7 | | eqid 2733 |
. . . . . 6
β’
(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) |
8 | | eqid 2733 |
. . . . . 6
β’
(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) |
9 | | 0cn 11155 |
. . . . . . . 8
β’ 0 β
β |
10 | 9 | elimel 4559 |
. . . . . . 7
β’ if(π΅ β β, π΅, 0) β
β |
11 | 10 | a1i 11 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if(π΅ β β, π΅, 0) β β) |
12 | 5, 6, 7, 8, 11 | iblcnlem1 25175 |
. . . . 5
β’ (π β ((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β πΏ1 β
((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β MblFn β§
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β)
β§ ((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β
β)))) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β ((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β πΏ1 β
((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β MblFn β§
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β)
β§ ((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β
β)))) |
14 | | eqid 2733 |
. . . . . 6
β’ π΄ = π΄ |
15 | | mbff 25012 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ π΅) β MblFn β (π₯ β π΄ β¦ π΅):dom (π₯ β π΄ β¦ π΅)βΆβ) |
16 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
17 | | itgcnlem.v |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β π΅ β π) |
18 | 16, 17 | dmmptd 6650 |
. . . . . . . . . . 11
β’ (π β dom (π₯ β π΄ β¦ π΅) = π΄) |
19 | 18 | feq2d 6658 |
. . . . . . . . . 10
β’ (π β ((π₯ β π΄ β¦ π΅):dom (π₯ β π΄ β¦ π΅)βΆβ β (π₯ β π΄ β¦ π΅):π΄βΆβ)) |
20 | 19 | biimpa 478 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ π΅):dom (π₯ β π΄ β¦ π΅)βΆβ) β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
21 | 15, 20 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
22 | 16 | fmpt 7062 |
. . . . . . . 8
β’
(βπ₯ β
π΄ π΅ β β β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
23 | 21, 22 | sylibr 233 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β βπ₯ β π΄ π΅ β β) |
24 | | iftrue 4496 |
. . . . . . . 8
β’ (π΅ β β β if(π΅ β β, π΅, 0) = π΅) |
25 | 24 | ralimi 3083 |
. . . . . . 7
β’
(βπ₯ β
π΄ π΅ β β β βπ₯ β π΄ if(π΅ β β, π΅, 0) = π΅) |
26 | 23, 25 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β βπ₯ β π΄ if(π΅ β β, π΅, 0) = π΅) |
27 | | mpteq12 5201 |
. . . . . 6
β’ ((π΄ = π΄ β§ βπ₯ β π΄ if(π΅ β β, π΅, 0) = π΅) β (π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) = (π₯ β π΄ β¦ π΅)) |
28 | 14, 26, 27 | sylancr 588 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) = (π₯ β π΄ β¦ π΅)) |
29 | 28 | eleq1d 2819 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β ((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β πΏ1 β
(π₯ β π΄ β¦ π΅) β
πΏ1)) |
30 | 28 | eleq1d 2819 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β ((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β MblFn β (π₯ β π΄ β¦ π΅) β MblFn)) |
31 | | eqid 2733 |
. . . . . . . . . 10
β’ β =
β |
32 | 24 | imim2i 16 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π΄ β π΅ β β) β (π₯ β π΄ β if(π΅ β β, π΅, 0) = π΅)) |
33 | 32 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β π΄ β π΅ β β) β§ π₯ β π΄) β if(π΅ β β, π΅, 0) = π΅) |
34 | 33 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π΄ β π΅ β β) β§ π₯ β π΄) β (ββif(π΅ β β, π΅, 0)) = (ββπ΅)) |
35 | 34 | ibllem 25152 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β π΅ β β) β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)) |
36 | 35 | a1d 25 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β π΅ β β) β (π₯ β β β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) |
37 | 36 | ralimi2 3078 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΄ π΅ β β β βπ₯ β β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)) |
38 | 23, 37 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β βπ₯ β β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)) |
39 | | mpteq12 5201 |
. . . . . . . . . 10
β’ ((β
= β β§ βπ₯
β β if((π₯ β
π΄ β§ 0 β€
(ββif(π΅ β
β, π΅, 0))),
(ββif(π΅ β
β, π΅, 0)), 0) =
if((π₯ β π΄ β§ 0 β€
(ββπ΅)),
(ββπ΅), 0))
β (π₯ β β
β¦ if((π₯ β π΄ β§ 0 β€
(ββif(π΅ β
β, π΅, 0))),
(ββif(π΅ β
β, π΅, 0)), 0)) =
(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€
(ββπ΅)),
(ββπ΅),
0))) |
40 | 31, 38, 39 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) |
41 | 40 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)))) |
42 | | itgcnlem.r |
. . . . . . . 8
β’ π
=
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) |
43 | 41, 42 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) = π
) |
44 | 43 | eleq1d 2819 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β
β π
β
β)) |
45 | 34 | negeqd 11403 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π΄ β π΅ β β) β§ π₯ β π΄) β -(ββif(π΅ β β, π΅, 0)) = -(ββπ΅)) |
46 | 45 | ibllem 25152 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β π΅ β β) β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)) |
47 | 46 | a1d 25 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β π΅ β β) β (π₯ β β β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) |
48 | 47 | ralimi2 3078 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΄ π΅ β β β βπ₯ β β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)) |
49 | 23, 48 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β βπ₯ β β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)) |
50 | | mpteq12 5201 |
. . . . . . . . . 10
β’ ((β
= β β§ βπ₯
β β if((π₯ β
π΄ β§ 0 β€
-(ββif(π΅ β
β, π΅, 0))),
-(ββif(π΅ β
β, π΅, 0)), 0) =
if((π₯ β π΄ β§ 0 β€
-(ββπ΅)),
-(ββπ΅), 0))
β (π₯ β β
β¦ if((π₯ β π΄ β§ 0 β€
-(ββif(π΅ β
β, π΅, 0))),
-(ββif(π΅ β
β, π΅, 0)), 0)) =
(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€
-(ββπ΅)),
-(ββπ΅),
0))) |
51 | 31, 49, 50 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) |
52 | 51 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)))) |
53 | | itgcnlem.s |
. . . . . . . 8
β’ π =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) |
54 | 52, 53 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) = π) |
55 | 54 | eleq1d 2819 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β
β π β
β)) |
56 | 44, 55 | anbi12d 632 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β)
β (π
β β
β§ π β
β))) |
57 | 33 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π΄ β π΅ β β) β§ π₯ β π΄) β (ββif(π΅ β β, π΅, 0)) = (ββπ΅)) |
58 | 57 | ibllem 25152 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β π΅ β β) β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)) |
59 | 58 | a1d 25 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β π΅ β β) β (π₯ β β β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) |
60 | 59 | ralimi2 3078 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΄ π΅ β β β βπ₯ β β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)) |
61 | 23, 60 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β βπ₯ β β if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)) |
62 | | mpteq12 5201 |
. . . . . . . . . 10
β’ ((β
= β β§ βπ₯
β β if((π₯ β
π΄ β§ 0 β€
(ββif(π΅ β
β, π΅, 0))),
(ββif(π΅ β
β, π΅, 0)), 0) =
if((π₯ β π΄ β§ 0 β€
(ββπ΅)),
(ββπ΅), 0))
β (π₯ β β
β¦ if((π₯ β π΄ β§ 0 β€
(ββif(π΅ β
β, π΅, 0))),
(ββif(π΅ β
β, π΅, 0)), 0)) =
(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€
(ββπ΅)),
(ββπ΅),
0))) |
63 | 31, 61, 62 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) |
64 | 63 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0)))) |
65 | | itgcnlem.t |
. . . . . . . 8
β’ π =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) |
66 | 64, 65 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) = π) |
67 | 66 | eleq1d 2819 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β
β π β
β)) |
68 | 57 | negeqd 11403 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π΄ β π΅ β β) β§ π₯ β π΄) β -(ββif(π΅ β β, π΅, 0)) = -(ββπ΅)) |
69 | 68 | ibllem 25152 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β π΅ β β) β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)) |
70 | 69 | a1d 25 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β π΅ β β) β (π₯ β β β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) |
71 | 70 | ralimi2 3078 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΄ π΅ β β β βπ₯ β β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)) |
72 | 23, 71 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β βπ₯ β β if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0) = if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)) |
73 | | mpteq12 5201 |
. . . . . . . . . 10
β’ ((β
= β β§ βπ₯
β β if((π₯ β
π΄ β§ 0 β€
-(ββif(π΅ β
β, π΅, 0))),
-(ββif(π΅ β
β, π΅, 0)), 0) =
if((π₯ β π΄ β§ 0 β€
-(ββπ΅)),
-(ββπ΅), 0))
β (π₯ β β
β¦ if((π₯ β π΄ β§ 0 β€
-(ββif(π΅ β
β, π΅, 0))),
-(ββif(π΅ β
β, π΅, 0)), 0)) =
(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€
-(ββπ΅)),
-(ββπ΅),
0))) |
74 | 31, 72, 73 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) |
75 | 74 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0)))) |
76 | | itgcnlem.u |
. . . . . . . 8
β’ π =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) |
77 | 75, 76 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) = π) |
78 | 77 | eleq1d 2819 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β
β π β
β)) |
79 | 67, 78 | anbi12d 632 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β
(((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β)
β (π β β
β§ π β
β))) |
80 | 30, 56, 79 | 3anbi123d 1437 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (((π₯ β π΄ β¦ if(π΅ β β, π΅, 0)) β MblFn β§
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β)
β§ ((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββif(π΅ β β, π΅, 0))), (ββif(π΅ β β, π΅, 0)), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββif(π΅ β β, π΅, 0))), -(ββif(π΅ β β, π΅, 0)), 0))) β β))
β ((π₯ β π΄ β¦ π΅) β MblFn β§ (π
β β β§ π β β) β§ (π β β β§ π β β)))) |
81 | 13, 29, 80 | 3bitr3d 309 |
. . 3
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β ((π₯ β π΄ β¦ π΅) β πΏ1 β
((π₯ β π΄ β¦ π΅) β MblFn β§ (π
β β β§ π β β) β§ (π β β β§ π β β)))) |
82 | 81 | ex 414 |
. 2
β’ (π β ((π₯ β π΄ β¦ π΅) β MblFn β ((π₯ β π΄ β¦ π΅) β πΏ1 β
((π₯ β π΄ β¦ π΅) β MblFn β§ (π
β β β§ π β β) β§ (π β β β§ π β β))))) |
83 | 2, 4, 82 | pm5.21ndd 381 |
1
β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β
((π₯ β π΄ β¦ π΅) β MblFn β§ (π
β β β§ π β β) β§ (π β β β§ π β β)))) |