Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-hgmap Unicode version

Definition df-hgmap 32077
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.)
Assertion
Ref Expression
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 ) ) ) ) } ) )
Distinct variable group:    a, b, k, m, u, v, w, x, y

Detailed syntax breakdown of Definition df-hgmap
StepHypRef Expression
1 chg 32076 . 2  class HGMap
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
8 va . . . . . . . . . 10  set  a
98cv 1622 . . . . . . . . 9  class  a
10 vx . . . . . . . . . 10  set  x
11 vb . . . . . . . . . . 11  set  b
1211cv 1622 . . . . . . . . . 10  class  b
1310cv 1622 . . . . . . . . . . . . . . 15  class  x
14 vv . . . . . . . . . . . . . . . 16  set  v
1514cv 1622 . . . . . . . . . . . . . . 15  class  v
16 vu . . . . . . . . . . . . . . . . 17  set  u
1716cv 1622 . . . . . . . . . . . . . . . 16  class  u
18 cvsca 13212 . . . . . . . . . . . . . . . 16  class  .s
1917, 18cfv 5255 . . . . . . . . . . . . . . 15  class  ( .s
`  u )
2013, 15, 19co 5858 . . . . . . . . . . . . . 14  class  ( x ( .s `  u
) v )
21 vm . . . . . . . . . . . . . . 15  set  m
2221cv 1622 . . . . . . . . . . . . . 14  class  m
2320, 22cfv 5255 . . . . . . . . . . . . 13  class  ( m `
 ( x ( .s `  u ) v ) )
24 vy . . . . . . . . . . . . . . 15  set  y
2524cv 1622 . . . . . . . . . . . . . 14  class  y
2615, 22cfv 5255 . . . . . . . . . . . . . 14  class  ( m `
 v )
274cv 1622 . . . . . . . . . . . . . . . 16  class  w
28 clcd 31776 . . . . . . . . . . . . . . . . 17  class LCDual
295, 28cfv 5255 . . . . . . . . . . . . . . . 16  class  (LCDual `  k )
3027, 29cfv 5255 . . . . . . . . . . . . . . 15  class  ( (LCDual `  k ) `  w
)
3130, 18cfv 5255 . . . . . . . . . . . . . 14  class  ( .s
`  ( (LCDual `  k ) `  w
) )
3225, 26, 31co 5858 . . . . . . . . . . . . 13  class  ( y ( .s `  (
(LCDual `  k ) `  w ) ) ( m `  v ) )
3323, 32wceq 1623 . . . . . . . . . . . 12  wff  ( m `
 ( x ( .s `  u ) v ) )  =  ( y ( .s
`  ( (LCDual `  k ) `  w
) ) ( m `
 v ) )
34 cbs 13148 . . . . . . . . . . . . 13  class  Base
3517, 34cfv 5255 . . . . . . . . . . . 12  class  ( Base `  u )
3633, 14, 35wral 2543 . . . . . . . . . . 11  wff  A. v  e.  ( Base `  u
) ( m `  ( x ( .s
`  u ) v ) )  =  ( y ( .s `  ( (LCDual `  k ) `  w ) ) ( m `  v ) )
3736, 24, 12crio 6297 . . . . . . . . . 10  class  ( iota_ y  e.  b A. v  e.  ( Base `  u
) ( m `  ( x ( .s
`  u ) v ) )  =  ( y ( .s `  ( (LCDual `  k ) `  w ) ) ( m `  v ) ) )
3810, 12, 37cmpt 4077 . . . . . . . . 9  class  ( x  e.  b  |->  ( iota_ y  e.  b A. v  e.  ( Base `  u
) ( m `  ( x ( .s
`  u ) v ) )  =  ( y ( .s `  ( (LCDual `  k ) `  w ) ) ( m `  v ) ) ) )
399, 38wcel 1684 . . . . . . . 8  wff  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 ) ) ) )
40 chdma 31983 . . . . . . . . . 10  class HDMap
415, 40cfv 5255 . . . . . . . . 9  class  (HDMap `  k )
4227, 41cfv 5255 . . . . . . . 8  class  ( (HDMap `  k ) `  w
)
4339, 21, 42wsbc 2991 . . . . . . 7  wff  [. (
(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 ) ) ) )
44 csca 13211 . . . . . . . . 9  class Scalar
4517, 44cfv 5255 . . . . . . . 8  class  (Scalar `  u )
4645, 34cfv 5255 . . . . . . 7  class  ( Base `  (Scalar `  u )
)
4743, 11, 46wsbc 2991 . . . . . 6  wff  [. ( 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 ) ) ) )
48 cdvh 31268 . . . . . . . 8  class  DVecH
495, 48cfv 5255 . . . . . . 7  class  ( DVecH `  k )
5027, 49cfv 5255 . . . . . 6  class  ( (
DVecH `  k ) `  w )
5147, 16, 50wsbc 2991 . . . . 5  wff  [. (
( 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 ) ) ) )
5251, 8cab 2269 . . . 4  class  { 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 ) ) ) ) }
534, 7, 52cmpt 4077 . . 3  class  ( 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 ) ) ) ) } )
542, 3, 53cmpt 4077 . 2  class  ( 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 ) ) ) ) } ) )
551, 54wceq 1623 1  wff 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 ) ) ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  hgmapffval  32078
  Copyright terms: Public domain W3C validator