Step | Hyp | Ref
| Expression |
1 | | diaval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | diaval.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | diaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | diaval.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
5 | | diaval.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
6 | | diaval.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
7 | 1, 2, 3, 4, 5, 6 | diafval 39523 |
. . . 4
β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})) |
8 | 7 | adantr 482 |
. . 3
β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})) |
9 | 8 | fveq1d 6849 |
. 2
β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = ((π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})βπ)) |
10 | | simpr 486 |
. . . 4
β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (π β π΅ β§ π β€ π)) |
11 | | breq1 5113 |
. . . . 5
β’ (π¦ = π β (π¦ β€ π β π β€ π)) |
12 | 11 | elrab 3650 |
. . . 4
β’ (π β {π¦ β π΅ β£ π¦ β€ π} β (π β π΅ β§ π β€ π)) |
13 | 10, 12 | sylibr 233 |
. . 3
β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β π β {π¦ β π΅ β£ π¦ β€ π}) |
14 | | breq2 5114 |
. . . . 5
β’ (π₯ = π β ((π
βπ) β€ π₯ β (π
βπ) β€ π)) |
15 | 14 | rabbidv 3418 |
. . . 4
β’ (π₯ = π β {π β π β£ (π
βπ) β€ π₯} = {π β π β£ (π
βπ) β€ π}) |
16 | | eqid 2737 |
. . . 4
β’ (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯}) = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯}) |
17 | 4 | fvexi 6861 |
. . . . 5
β’ π β V |
18 | 17 | rabex 5294 |
. . . 4
β’ {π β π β£ (π
βπ) β€ π} β V |
19 | 15, 16, 18 | fvmpt 6953 |
. . 3
β’ (π β {π¦ β π΅ β£ π¦ β€ π} β ((π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})βπ) = {π β π β£ (π
βπ) β€ π}) |
20 | 13, 19 | syl 17 |
. 2
β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β ((π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})βπ) = {π β π β£ (π
βπ) β€ π}) |
21 | 9, 20 | eqtrd 2777 |
1
β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β π β£ (π
βπ) β€ π}) |