Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6846 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | diaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2791 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
6 | | diaval.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = π΅) |
8 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
9 | | diaval.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (leβπ) = β€ ) |
11 | 10 | breqd 5120 |
. . . . . 6
β’ (π = πΎ β (π¦(leβπ)π€ β π¦ β€ π€)) |
12 | 7, 11 | rabeqbidv 3423 |
. . . . 5
β’ (π = πΎ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} = {π¦ β π΅ β£ π¦ β€ π€}) |
13 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
14 | 13 | fveq1d 6848 |
. . . . . 6
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
15 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = πΎ β (trLβπ) = (trLβπΎ)) |
16 | 15 | fveq1d 6848 |
. . . . . . . 8
β’ (π = πΎ β ((trLβπ)βπ€) = ((trLβπΎ)βπ€)) |
17 | 16 | fveq1d 6848 |
. . . . . . 7
β’ (π = πΎ β (((trLβπ)βπ€)βπ) = (((trLβπΎ)βπ€)βπ)) |
18 | | eqidd 2734 |
. . . . . . 7
β’ (π = πΎ β π₯ = π₯) |
19 | 17, 10, 18 | breq123d 5123 |
. . . . . 6
β’ (π = πΎ β ((((trLβπ)βπ€)βπ)(leβπ)π₯ β (((trLβπΎ)βπ€)βπ) β€ π₯)) |
20 | 14, 19 | rabeqbidv 3423 |
. . . . 5
β’ (π = πΎ β {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯} = {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}) |
21 | 12, 20 | mpteq12dv 5200 |
. . . 4
β’ (π = πΎ β (π₯ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} β¦ {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯}) = (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯})) |
22 | 4, 21 | mpteq12dv 5200 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ (π₯ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} β¦ {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯})) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) |
23 | | df-disoa 39542 |
. . 3
β’ DIsoA =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} β¦ {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯}))) |
24 | 22, 23, 3 | mptfvmpt 7182 |
. 2
β’ (πΎ β V β
(DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) |
25 | 1, 24 | syl 17 |
1
β’ (πΎ β π β (DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) |