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 ) ) ) ) } ) )