Step | Hyp | Ref
| Expression |
1 | | hsphoival.h |
. . . 4
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
2 | | breq2 5153 |
. . . . . . . 8
β’ (π₯ = π΄ β ((πβπ) β€ π₯ β (πβπ) β€ π΄)) |
3 | | id 22 |
. . . . . . . 8
β’ (π₯ = π΄ β π₯ = π΄) |
4 | 2, 3 | ifbieq2d 4555 |
. . . . . . 7
β’ (π₯ = π΄ β if((πβπ) β€ π₯, (πβπ), π₯) = if((πβπ) β€ π΄, (πβπ), π΄)) |
5 | 4 | ifeq2d 4549 |
. . . . . 6
β’ (π₯ = π΄ β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄))) |
6 | 5 | mpteq2dv 5251 |
. . . . 5
β’ (π₯ = π΄ β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄)))) |
7 | 6 | mpteq2dv 5251 |
. . . 4
β’ (π₯ = π΄ β (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) = (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄))))) |
8 | | hsphoival.a |
. . . 4
β’ (π β π΄ β β) |
9 | | ovex 7442 |
. . . . . 6
β’ (β
βm π)
β V |
10 | 9 | mptex 7225 |
. . . . 5
β’ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄)))) β V |
11 | 10 | a1i 11 |
. . . 4
β’ (π β (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄)))) β V) |
12 | 1, 7, 8, 11 | fvmptd3 7022 |
. . 3
β’ (π β (π»βπ΄) = (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄))))) |
13 | | fveq1 6891 |
. . . . . 6
β’ (π = π΅ β (πβπ) = (π΅βπ)) |
14 | 13 | breq1d 5159 |
. . . . . . 7
β’ (π = π΅ β ((πβπ) β€ π΄ β (π΅βπ) β€ π΄)) |
15 | 14, 13 | ifbieq1d 4553 |
. . . . . 6
β’ (π = π΅ β if((πβπ) β€ π΄, (πβπ), π΄) = if((π΅βπ) β€ π΄, (π΅βπ), π΄)) |
16 | 13, 15 | ifeq12d 4550 |
. . . . 5
β’ (π = π΅ β if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄)) = if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄))) |
17 | 16 | mpteq2dv 5251 |
. . . 4
β’ (π = π΅ β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄))) = (π β π β¦ if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄)))) |
18 | 17 | adantl 483 |
. . 3
β’ ((π β§ π = π΅) β (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π΄, (πβπ), π΄))) = (π β π β¦ if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄)))) |
19 | | hsphoival.b |
. . . 4
β’ (π β π΅:πβΆβ) |
20 | | reex 11201 |
. . . . . . 7
β’ β
β V |
21 | 20 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
22 | | hsphoival.x |
. . . . . 6
β’ (π β π β π) |
23 | 21, 22 | jca 513 |
. . . . 5
β’ (π β (β β V β§
π β π)) |
24 | | elmapg 8833 |
. . . . 5
β’ ((β
β V β§ π β
π) β (π΅ β (β
βm π)
β π΅:πβΆβ)) |
25 | 23, 24 | syl 17 |
. . . 4
β’ (π β (π΅ β (β βm π) β π΅:πβΆβ)) |
26 | 19, 25 | mpbird 257 |
. . 3
β’ (π β π΅ β (β βm π)) |
27 | | mptexg 7223 |
. . . 4
β’ (π β π β (π β π β¦ if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄))) β V) |
28 | 22, 27 | syl 17 |
. . 3
β’ (π β (π β π β¦ if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄))) β V) |
29 | 12, 18, 26, 28 | fvmptd 7006 |
. 2
β’ (π β ((π»βπ΄)βπ΅) = (π β π β¦ if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄)))) |
30 | | eleq1 2822 |
. . . 4
β’ (π = πΎ β (π β π β πΎ β π)) |
31 | | fveq2 6892 |
. . . 4
β’ (π = πΎ β (π΅βπ) = (π΅βπΎ)) |
32 | 31 | breq1d 5159 |
. . . . 5
β’ (π = πΎ β ((π΅βπ) β€ π΄ β (π΅βπΎ) β€ π΄)) |
33 | 32, 31 | ifbieq1d 4553 |
. . . 4
β’ (π = πΎ β if((π΅βπ) β€ π΄, (π΅βπ), π΄) = if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄)) |
34 | 30, 31, 33 | ifbieq12d 4557 |
. . 3
β’ (π = πΎ β if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄)) = if(πΎ β π, (π΅βπΎ), if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄))) |
35 | 34 | adantl 483 |
. 2
β’ ((π β§ π = πΎ) β if(π β π, (π΅βπ), if((π΅βπ) β€ π΄, (π΅βπ), π΄)) = if(πΎ β π, (π΅βπΎ), if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄))) |
36 | | hsphoival.k |
. 2
β’ (π β πΎ β π) |
37 | 19, 36 | ffvelcdmd 7088 |
. . 3
β’ (π β (π΅βπΎ) β β) |
38 | 37, 8 | ifcld 4575 |
. . 3
β’ (π β if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄) β β) |
39 | 37, 38 | ifexd 4577 |
. 2
β’ (π β if(πΎ β π, (π΅βπΎ), if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄)) β V) |
40 | 29, 35, 36, 39 | fvmptd 7006 |
1
β’ (π β (((π»βπ΄)βπ΅)βπΎ) = if(πΎ β π, (π΅βπΎ), if((π΅βπΎ) β€ π΄, (π΅βπΎ), π΄))) |