# 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
`|- HGMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chg
` |-  HGMap`
1 vk
` |-  k`
2 cvv
` |-  _V`
3 vw
` |-  w`
4 clh
` |-  LHyp`
5 1 cv
` |-  k`
6 5 4 cfv
` |-  ( LHyp ` k )`
7 va
` |-  a`
8 cdvh
` |-  DVecH`
9 5 8 cfv
` |-  ( DVecH ` k )`
10 3 cv
` |-  w`
11 10 9 cfv
` |-  ( ( DVecH ` k ) ` w )`
12 vu
` |-  u`
13 cbs
` |-  Base`
14 csca
` |-  Scalar`
15 12 cv
` |-  u`
16 15 14 cfv
` |-  ( Scalar ` u )`
17 16 13 cfv
` |-  ( Base ` ( Scalar ` u ) )`
18 vb
` |-  b`
19 chdma
` |-  HDMap`
20 5 19 cfv
` |-  ( HDMap ` k )`
21 10 20 cfv
` |-  ( ( HDMap ` k ) ` w )`
22 vm
` |-  m`
23 7 cv
` |-  a`
24 vx
` |-  x`
25 18 cv
` |-  b`
26 vy
` |-  y`
27 vv
` |-  v`
28 15 13 cfv
` |-  ( Base ` u )`
29 22 cv
` |-  m`
30 24 cv
` |-  x`
31 cvsca
` |-  .s`
32 15 31 cfv
` |-  ( .s ` u )`
33 27 cv
` |-  v`
34 30 33 32 co
` |-  ( x ( .s ` u ) v )`
35 34 29 cfv
` |-  ( m ` ( x ( .s ` u ) v ) )`
36 26 cv
` |-  y`
37 clcd
` |-  LCDual`
38 5 37 cfv
` |-  ( LCDual ` k )`
39 10 38 cfv
` |-  ( ( LCDual ` k ) ` w )`
40 39 31 cfv
` |-  ( .s ` ( ( LCDual ` k ) ` w ) )`
41 33 29 cfv
` |-  ( m ` v )`
42 36 41 40 co
` |-  ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) )`
43 35 42 wceq
` |-  ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) )`
44 43 27 28 wral
` |-  A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) )`
45 44 26 25 crio
` |-  ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) )`
46 24 25 45 cmpt
` |-  ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) )`
47 23 46 wcel
` |-  a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) )`
48 47 22 21 wsbc
` |-  [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) )`
49 48 18 17 wsbc
` |-  [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) )`
50 49 12 11 wsbc
` |-  [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) )`
51 50 7 cab
` |-  { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) }`
52 3 6 51 cmpt
` |-  ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } )`
53 1 2 52 cmpt
` |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )`
54 0 53 wceq
` |-  HGMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` ( Scalar ` u ) ) / b ]. [. ( ( HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( ( LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )`