Step | Hyp | Ref
| Expression |
1 | | lcdval.k |
. 2
β’ (π β (πΎ β π β§ π β π»)) |
2 | | lcdval.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
3 | | lcdval.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
4 | 3 | lcdfval 40459 |
. . . . 5
β’ (πΎ β π β (LCDualβπΎ) = (π€ β π» β¦ ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)}))) |
5 | 4 | fveq1d 6894 |
. . . 4
β’ (πΎ β π β ((LCDualβπΎ)βπ) = ((π€ β π» β¦ ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)}))βπ)) |
6 | 2, 5 | eqtrid 2785 |
. . 3
β’ (πΎ β π β πΆ = ((π€ β π» β¦ ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)}))βπ)) |
7 | | fveq2 6892 |
. . . . . . . 8
β’ (π€ = π β ((DVecHβπΎ)βπ€) = ((DVecHβπΎ)βπ)) |
8 | | lcdval.u |
. . . . . . . 8
β’ π = ((DVecHβπΎ)βπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β ((DVecHβπΎ)βπ€) = π) |
10 | 9 | fveq2d 6896 |
. . . . . 6
β’ (π€ = π β (LDualβ((DVecHβπΎ)βπ€)) = (LDualβπ)) |
11 | | lcdval.d |
. . . . . 6
β’ π· = (LDualβπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (LDualβ((DVecHβπΎ)βπ€)) = π·) |
13 | 9 | fveq2d 6896 |
. . . . . . 7
β’ (π€ = π β (LFnlβ((DVecHβπΎ)βπ€)) = (LFnlβπ)) |
14 | | lcdval.f |
. . . . . . 7
β’ πΉ = (LFnlβπ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (LFnlβ((DVecHβπΎ)βπ€)) = πΉ) |
16 | | fveq2 6892 |
. . . . . . . . 9
β’ (π€ = π β ((ocHβπΎ)βπ€) = ((ocHβπΎ)βπ)) |
17 | | lcdval.o |
. . . . . . . . 9
β’ β₯ =
((ocHβπΎ)βπ) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β ((ocHβπΎ)βπ€) = β₯ ) |
19 | 9 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π€ = π β (LKerβ((DVecHβπΎ)βπ€)) = (LKerβπ)) |
20 | | lcdval.l |
. . . . . . . . . . 11
β’ πΏ = (LKerβπ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π€ = π β (LKerβ((DVecHβπΎ)βπ€)) = πΏ) |
22 | 21 | fveq1d 6894 |
. . . . . . . . 9
β’ (π€ = π β ((LKerβ((DVecHβπΎ)βπ€))βπ) = (πΏβπ)) |
23 | 18, 22 | fveq12d 6899 |
. . . . . . . 8
β’ (π€ = π β (((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ)) = ( β₯ β(πΏβπ))) |
24 | 18, 23 | fveq12d 6899 |
. . . . . . 7
β’ (π€ = π β (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ( β₯ β( β₯
β(πΏβπ)))) |
25 | 24, 22 | eqeq12d 2749 |
. . . . . 6
β’ (π€ = π β ((((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ) β ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ))) |
26 | 15, 25 | rabeqbidv 3450 |
. . . . 5
β’ (π€ = π β {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)} = {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)}) |
27 | 12, 26 | oveq12d 7427 |
. . . 4
β’ (π€ = π β ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)}) = (π· βΎs {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)})) |
28 | | eqid 2733 |
. . . 4
β’ (π€ β π» β¦ ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)})) = (π€ β π» β¦ ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)})) |
29 | | ovex 7442 |
. . . 4
β’ (π· βΎs {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)}) β V |
30 | 27, 28, 29 | fvmpt 6999 |
. . 3
β’ (π β π» β ((π€ β π» β¦ ((LDualβ((DVecHβπΎ)βπ€)) βΎs {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ (((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ)}))βπ) = (π· βΎs {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)})) |
31 | 6, 30 | sylan9eq 2793 |
. 2
β’ ((πΎ β π β§ π β π») β πΆ = (π· βΎs {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)})) |
32 | 1, 31 | syl 17 |
1
β’ (π β πΆ = (π· βΎs {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)})) |