Step | Hyp | Ref
| Expression |
1 | | hoidifhspval2.d |
. . 3
β’ π· = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π₯ β€ (πβπ), (πβπ), π₯), (πβπ))))) |
2 | | hoidifhspval2.y |
. . 3
β’ (π β π β β) |
3 | 1, 2 | hoidifhspval 45002 |
. 2
β’ (π β (π·βπ) = (π β (β βm π) β¦ (π β π β¦ if(π = πΎ, if(π β€ (πβπ), (πβπ), π), (πβπ))))) |
4 | | fveq1 6861 |
. . . . . . 7
β’ (π = π΄ β (πβπ) = (π΄βπ)) |
5 | 4 | breq2d 5137 |
. . . . . 6
β’ (π = π΄ β (π β€ (πβπ) β π β€ (π΄βπ))) |
6 | 5, 4 | ifbieq1d 4530 |
. . . . 5
β’ (π = π΄ β if(π β€ (πβπ), (πβπ), π) = if(π β€ (π΄βπ), (π΄βπ), π)) |
7 | 6, 4 | ifeq12d 4527 |
. . . 4
β’ (π = π΄ β if(π = πΎ, if(π β€ (πβπ), (πβπ), π), (πβπ)) = if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ))) |
8 | 7 | mpteq2dv 5227 |
. . 3
β’ (π = π΄ β (π β π β¦ if(π = πΎ, if(π β€ (πβπ), (πβπ), π), (πβπ))) = (π β π β¦ if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ)))) |
9 | 8 | adantl 482 |
. 2
β’ ((π β§ π = π΄) β (π β π β¦ if(π = πΎ, if(π β€ (πβπ), (πβπ), π), (πβπ))) = (π β π β¦ if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ)))) |
10 | | hoidifhspval2.a |
. . 3
β’ (π β π΄:πβΆβ) |
11 | | reex 11166 |
. . . . . 6
β’ β
β V |
12 | 11 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
13 | | hoidifhspval2.x |
. . . . 5
β’ (π β π β π) |
14 | 12, 13 | jca 512 |
. . . 4
β’ (π β (β β V β§
π β π)) |
15 | | elmapg 8800 |
. . . 4
β’ ((β
β V β§ π β
π) β (π΄ β (β
βm π)
β π΄:πβΆβ)) |
16 | 14, 15 | syl 17 |
. . 3
β’ (π β (π΄ β (β βm π) β π΄:πβΆβ)) |
17 | 10, 16 | mpbird 256 |
. 2
β’ (π β π΄ β (β βm π)) |
18 | | mptexg 7191 |
. . 3
β’ (π β π β (π β π β¦ if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ))) β V) |
19 | 13, 18 | syl 17 |
. 2
β’ (π β (π β π β¦ if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ))) β V) |
20 | 3, 9, 17, 19 | fvmptd 6975 |
1
β’ (π β ((π·βπ)βπ΄) = (π β π β¦ if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ)))) |