Step | Hyp | Ref
| Expression |
1 | | diaval.i |
. . 3
β’ πΌ = ((DIsoAβπΎ)βπ) |
2 | | diaval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | diaval.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | diaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | 2, 3, 4 | diaffval 39522 |
. . . 4
β’ (πΎ β π β (DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) |
6 | 5 | fveq1d 6849 |
. . 3
β’ (πΎ β π β ((DIsoAβπΎ)βπ) = ((π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))βπ)) |
7 | 1, 6 | eqtrid 2789 |
. 2
β’ (πΎ β π β πΌ = ((π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))βπ)) |
8 | | breq2 5114 |
. . . . 5
β’ (π€ = π β (π¦ β€ π€ β π¦ β€ π)) |
9 | 8 | rabbidv 3418 |
. . . 4
β’ (π€ = π β {π¦ β π΅ β£ π¦ β€ π€} = {π¦ β π΅ β£ π¦ β€ π}) |
10 | | fveq2 6847 |
. . . . . 6
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
11 | | diaval.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
13 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π β ((trLβπΎ)βπ€) = ((trLβπΎ)βπ)) |
14 | | diaval.r |
. . . . . . . 8
β’ π
= ((trLβπΎ)βπ) |
15 | 13, 14 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β ((trLβπΎ)βπ€) = π
) |
16 | 15 | fveq1d 6849 |
. . . . . 6
β’ (π€ = π β (((trLβπΎ)βπ€)βπ) = (π
βπ)) |
17 | 16 | breq1d 5120 |
. . . . 5
β’ (π€ = π β ((((trLβπΎ)βπ€)βπ) β€ π₯ β (π
βπ) β€ π₯)) |
18 | 12, 17 | rabeqbidv 3427 |
. . . 4
β’ (π€ = π β {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯} = {π β π β£ (π
βπ) β€ π₯}) |
19 | 9, 18 | mpteq12dv 5201 |
. . 3
β’ (π€ = π β (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}) = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})) |
20 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯})) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯})) |
21 | 2 | fvexi 6861 |
. . . 4
β’ π΅ β V |
22 | 21 | mptrabex 7180 |
. . 3
β’ (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯}) β V |
23 | 19, 20, 22 | fvmpt 6953 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))βπ) = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})) |
24 | 7, 23 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π
βπ) β€ π₯})) |