# Metamath Proof Explorer

## Definition df-hgmap

Description: Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

Ref Expression
Assertion df-hgmap

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chg ${class}\mathrm{HGMap}$
1 vk ${setvar}{k}$
2 cvv ${class}\mathrm{V}$
3 vw ${setvar}{w}$
4 clh ${class}\mathrm{LHyp}$
5 1 cv ${setvar}{k}$
6 5 4 cfv ${class}\mathrm{LHyp}\left({k}\right)$
7 va ${setvar}{a}$
8 cdvh ${class}\mathrm{DVecH}$
9 5 8 cfv ${class}\mathrm{DVecH}\left({k}\right)$
10 3 cv ${setvar}{w}$
11 10 9 cfv ${class}\mathrm{DVecH}\left({k}\right)\left({w}\right)$
12 vu ${setvar}{u}$
13 cbs ${class}\mathrm{Base}$
14 csca ${class}\mathrm{Scalar}$
15 12 cv ${setvar}{u}$
16 15 14 cfv ${class}\mathrm{Scalar}\left({u}\right)$
17 16 13 cfv ${class}{\mathrm{Base}}_{\mathrm{Scalar}\left({u}\right)}$
18 vb ${setvar}{b}$
19 chdma ${class}\mathrm{HDMap}$
20 5 19 cfv ${class}\mathrm{HDMap}\left({k}\right)$
21 10 20 cfv ${class}\mathrm{HDMap}\left({k}\right)\left({w}\right)$
22 vm ${setvar}{m}$
23 7 cv ${setvar}{a}$
24 vx ${setvar}{x}$
25 18 cv ${setvar}{b}$
26 vy ${setvar}{y}$
27 vv ${setvar}{v}$
28 15 13 cfv ${class}{\mathrm{Base}}_{{u}}$
29 22 cv ${setvar}{m}$
30 24 cv ${setvar}{x}$
31 cvsca ${class}{\cdot }_{𝑠}$
32 15 31 cfv ${class}{\cdot }_{{u}}$
33 27 cv ${setvar}{v}$
34 30 33 32 co ${class}\left({x}{\cdot }_{{u}}{v}\right)$
35 34 29 cfv ${class}{m}\left({x}{\cdot }_{{u}}{v}\right)$
36 26 cv ${setvar}{y}$
37 clcd ${class}\mathrm{LCDual}$
38 5 37 cfv ${class}\mathrm{LCDual}\left({k}\right)$
39 10 38 cfv ${class}\mathrm{LCDual}\left({k}\right)\left({w}\right)$
40 39 31 cfv ${class}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}$
41 33 29 cfv ${class}{m}\left({v}\right)$
42 36 41 40 co ${class}\left({y}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}{m}\left({v}\right)\right)$
43 35 42 wceq ${wff}{m}\left({x}{\cdot }_{{u}}{v}\right)={y}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}{m}\left({v}\right)$
44 43 27 28 wral ${wff}\forall {v}\in {\mathrm{Base}}_{{u}}\phantom{\rule{.4em}{0ex}}{m}\left({x}{\cdot }_{{u}}{v}\right)={y}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}{m}\left({v}\right)$
45 44 26 25 crio ${class}\left(\iota {y}\in {b}|\forall {v}\in {\mathrm{Base}}_{{u}}\phantom{\rule{.4em}{0ex}}{m}\left({x}{\cdot }_{{u}}{v}\right)={y}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}{m}\left({v}\right)\right)$
46 24 25 45 cmpt ${class}\left({x}\in {b}⟼\left(\iota {y}\in {b}|\forall {v}\in {\mathrm{Base}}_{{u}}\phantom{\rule{.4em}{0ex}}{m}\left({x}{\cdot }_{{u}}{v}\right)={y}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}{m}\left({v}\right)\right)\right)$
47 23 46 wcel ${wff}{a}\in \left({x}\in {b}⟼\left(\iota {y}\in {b}|\forall {v}\in {\mathrm{Base}}_{{u}}\phantom{\rule{.4em}{0ex}}{m}\left({x}{\cdot }_{{u}}{v}\right)={y}{\cdot }_{\mathrm{LCDual}\left({k}\right)\left({w}\right)}{m}\left({v}\right)\right)\right)$
48 47 22 21 wsbc
49 48 18 17 wsbc
50 49 12 11 wsbc
51 50 7 cab
52 3 6 51 cmpt
53 1 2 52 cmpt
54 0 53 wceq