Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6846 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | dochval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2791 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (DVecHβπ) = (DVecHβπΎ)) |
6 | 5 | fveq1d 6848 |
. . . . . . 7
β’ (π = πΎ β ((DVecHβπ)βπ€) = ((DVecHβπΎ)βπ€)) |
7 | 6 | fveq2d 6850 |
. . . . . 6
β’ (π = πΎ β (Baseβ((DVecHβπ)βπ€)) = (Baseβ((DVecHβπΎ)βπ€))) |
8 | 7 | pweqd 4581 |
. . . . 5
β’ (π = πΎ β π«
(Baseβ((DVecHβπ)βπ€)) = π«
(Baseβ((DVecHβπΎ)βπ€))) |
9 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (DIsoHβπ) = (DIsoHβπΎ)) |
10 | 9 | fveq1d 6848 |
. . . . . 6
β’ (π = πΎ β ((DIsoHβπ)βπ€) = ((DIsoHβπΎ)βπ€)) |
11 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (ocβπ) = (ocβπΎ)) |
12 | | dochval.o |
. . . . . . . 8
β’ β₯ =
(ocβπΎ) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (ocβπ) = β₯ ) |
14 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = πΎ β (glbβπ) = (glbβπΎ)) |
15 | | dochval.g |
. . . . . . . . 9
β’ πΊ = (glbβπΎ) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΎ β (glbβπ) = πΊ) |
17 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
18 | | dochval.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π = πΎ β (Baseβπ) = π΅) |
20 | 10 | fveq1d 6848 |
. . . . . . . . . 10
β’ (π = πΎ β (((DIsoHβπ)βπ€)βπ¦) = (((DIsoHβπΎ)βπ€)βπ¦)) |
21 | 20 | sseq2d 3980 |
. . . . . . . . 9
β’ (π = πΎ β (π₯ β (((DIsoHβπ)βπ€)βπ¦) β π₯ β (((DIsoHβπΎ)βπ€)βπ¦))) |
22 | 19, 21 | rabeqbidv 3423 |
. . . . . . . 8
β’ (π = πΎ β {π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)} = {π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}) |
23 | 16, 22 | fveq12d 6853 |
. . . . . . 7
β’ (π = πΎ β ((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)}) = (πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})) |
24 | 13, 23 | fveq12d 6853 |
. . . . . 6
β’ (π = πΎ β ((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})) = ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}))) |
25 | 10, 24 | fveq12d 6853 |
. . . . 5
β’ (π = πΎ β (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)}))) = (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))) |
26 | 8, 25 | mpteq12dv 5200 |
. . . 4
β’ (π = πΎ β (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})))) = (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)}))))) |
27 | 4, 26 | mpteq12dv 5200 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)}))))) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))) |
28 | | df-doch 39861 |
. . 3
β’ ocH =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})))))) |
29 | 27, 28, 3 | mptfvmpt 7182 |
. 2
β’ (πΎ β V β
(ocHβπΎ) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))) |
30 | 1, 29 | syl 17 |
1
β’ (πΎ β π β (ocHβπΎ) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))) |