Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6843 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | hgmapval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (DVecHβπ) = (DVecHβπΎ)) |
6 | 5 | fveq1d 6845 |
. . . . . 6
β’ (π = πΎ β ((DVecHβπ)βπ€) = ((DVecHβπΎ)βπ€)) |
7 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (HDMapβπ) = (HDMapβπΎ)) |
8 | 7 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β ((HDMapβπ)βπ€) = ((HDMapβπΎ)βπ€)) |
9 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π = πΎ β (LCDualβπ) = (LCDualβπΎ)) |
10 | 9 | fveq1d 6845 |
. . . . . . . . . . . . . . 15
β’ (π = πΎ β ((LCDualβπ)βπ€) = ((LCDualβπΎ)βπ€)) |
11 | 10 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (π = πΎ β (
Β·π β((LCDualβπ)βπ€)) = ( Β·π
β((LCDualβπΎ)βπ€))) |
12 | 11 | oveqd 7375 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£))) |
13 | 12 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π = πΎ β ((πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)) β (πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))) |
14 | 13 | ralbidv 3175 |
. . . . . . . . . . 11
β’ (π = πΎ β (βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)) β βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))) |
15 | 14 | riotabidv 7316 |
. . . . . . . . . 10
β’ (π = πΎ β (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))) = (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))) |
16 | 15 | mpteq2dv 5208 |
. . . . . . . . 9
β’ (π = πΎ β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) = (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£))))) |
17 | 16 | eleq2d 2824 |
. . . . . . . 8
β’ (π = πΎ β (π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) β π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))))) |
18 | 8, 17 | sbceqbid 3747 |
. . . . . . 7
β’ (π = πΎ β ([((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) β [((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))))) |
19 | 18 | sbcbidv 3799 |
. . . . . 6
β’ (π = πΎ β
([(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) β
[(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))))) |
20 | 6, 19 | sbceqbid 3747 |
. . . . 5
β’ (π = πΎ β ([((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£)))) β [((DVecHβπΎ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£)))))) |
21 | 20 | abbidv 2806 |
. . . 4
β’ (π = πΎ β {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))} = {π β£ [((DVecHβπΎ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£))))}) |
22 | 4, 21 | mpteq12dv 5197 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))}) = (π€ β π» β¦ {π β£ [((DVecHβπΎ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£))))})) |
23 | | df-hgmap 40350 |
. . 3
β’ HGMap =
(π β V β¦ (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπ)βπ€))(πβπ£))))})) |
24 | 22, 23, 3 | mptfvmpt 7179 |
. 2
β’ (πΎ β V β
(HGMapβπΎ) = (π€ β π» β¦ {π β£ [((DVecHβπΎ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£))))})) |
25 | 1, 24 | syl 17 |
1
β’ (πΎ β π β (HGMapβπΎ) = (π€ β π» β¦ {π β£ [((DVecHβπΎ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π
βπ’)π£)) = (π¦( Β·π
β((LCDualβπΎ)βπ€))(πβπ£))))})) |