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

Definition df-hdmap 31985
Description: Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 32020 description for more details. (Contributed by NM, 15-May-2015.)
Assertion
Ref Expression
df-hdmap  |- HDMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. <. (  _I  |`  ( Base `  k
) ) ,  (  _I  |`  ( ( LTrn `  k ) `  w ) ) >.  /  e ]. [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) ) } ) )
Distinct variable group:    e, a, i, k, t, u, v, w, y, z

Detailed syntax breakdown of Definition df-hdmap
StepHypRef Expression
1 chdma 31983 . 2  class HDMap
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 . . . . . . . . . . 11  set  a
98cv 1622 . . . . . . . . . 10  class  a
10 vt . . . . . . . . . . 11  set  t
11 vv . . . . . . . . . . . 12  set  v
1211cv 1622 . . . . . . . . . . 11  class  v
13 vz . . . . . . . . . . . . . . . . 17  set  z
1413cv 1622 . . . . . . . . . . . . . . . 16  class  z
15 ve . . . . . . . . . . . . . . . . . . . 20  set  e
1615cv 1622 . . . . . . . . . . . . . . . . . . 19  class  e
1716csn 3640 . . . . . . . . . . . . . . . . . 18  class  { e }
18 vu . . . . . . . . . . . . . . . . . . . 20  set  u
1918cv 1622 . . . . . . . . . . . . . . . . . . 19  class  u
20 clspn 15728 . . . . . . . . . . . . . . . . . . 19  class  LSpan
2119, 20cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( LSpan `  u )
2217, 21cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( (
LSpan `  u ) `  { e } )
2310cv 1622 . . . . . . . . . . . . . . . . . . 19  class  t
2423csn 3640 . . . . . . . . . . . . . . . . . 18  class  { t }
2524, 21cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( (
LSpan `  u ) `  { t } )
2622, 25cun 3150 . . . . . . . . . . . . . . . 16  class  ( ( ( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )
2714, 26wcel 1684 . . . . . . . . . . . . . . 15  wff  z  e.  ( ( ( LSpan `  u ) `  {
e } )  u.  ( ( LSpan `  u
) `  { t } ) )
2827wn 3 . . . . . . . . . . . . . 14  wff  -.  z  e.  ( ( ( LSpan `  u ) `  {
e } )  u.  ( ( LSpan `  u
) `  { t } ) )
29 vy . . . . . . . . . . . . . . . 16  set  y
3029cv 1622 . . . . . . . . . . . . . . 15  class  y
314cv 1622 . . . . . . . . . . . . . . . . . . . . 21  class  w
32 chvm 31946 . . . . . . . . . . . . . . . . . . . . . 22  class HVMap
335, 32cfv 5255 . . . . . . . . . . . . . . . . . . . . 21  class  (HVMap `  k )
3431, 33cfv 5255 . . . . . . . . . . . . . . . . . . . 20  class  ( (HVMap `  k ) `  w
)
3516, 34cfv 5255 . . . . . . . . . . . . . . . . . . 19  class  ( ( (HVMap `  k ) `  w ) `  e
)
3616, 35, 14cotp 3644 . . . . . . . . . . . . . . . . . 18  class  <. e ,  ( ( (HVMap `  k ) `  w
) `  e ) ,  z >.
37 vi . . . . . . . . . . . . . . . . . . 19  set  i
3837cv 1622 . . . . . . . . . . . . . . . . . 18  class  i
3936, 38cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( i `
 <. e ,  ( ( (HVMap `  k
) `  w ) `  e ) ,  z
>. )
4014, 39, 23cotp 3644 . . . . . . . . . . . . . . . 16  class  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
4140, 38cfv 5255 . . . . . . . . . . . . . . 15  class  ( i `
 <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w
) `  e ) ,  z >. ) ,  t >. )
4230, 41wceq 1623 . . . . . . . . . . . . . 14  wff  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
)
4328, 42wi 4 . . . . . . . . . . . . 13  wff  ( -.  z  e.  ( ( ( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) )
4443, 13, 12wral 2543 . . . . . . . . . . . 12  wff  A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) )
45 clcd 31776 . . . . . . . . . . . . . . 15  class LCDual
465, 45cfv 5255 . . . . . . . . . . . . . 14  class  (LCDual `  k )
4731, 46cfv 5255 . . . . . . . . . . . . 13  class  ( (LCDual `  k ) `  w
)
48 cbs 13148 . . . . . . . . . . . . 13  class  Base
4947, 48cfv 5255 . . . . . . . . . . . 12  class  ( Base `  ( (LCDual `  k
) `  w )
)
5044, 29, 49crio 6297 . . . . . . . . . . 11  class  ( iota_ y  e.  ( Base `  (
(LCDual `  k ) `  w ) ) A. z  e.  v  ( -.  z  e.  (
( ( LSpan `  u
) `  { e } )  u.  (
( LSpan `  u ) `  { t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) )
5110, 12, 50cmpt 4077 . . . . . . . . . 10  class  ( t  e.  v  |->  ( iota_ y  e.  ( Base `  (
(LCDual `  k ) `  w ) ) A. z  e.  v  ( -.  z  e.  (
( ( LSpan `  u
) `  { e } )  u.  (
( LSpan `  u ) `  { t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) )
529, 51wcel 1684 . . . . . . . . 9  wff  a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) )
53 chdma1 31982 . . . . . . . . . . 11  class HDMap1
545, 53cfv 5255 . . . . . . . . . 10  class  (HDMap1 `  k )
5531, 54cfv 5255 . . . . . . . . 9  class  ( (HDMap1 `  k ) `  w
)
5652, 37, 55wsbc 2991 . . . . . . . 8  wff  [. (
(HDMap1 `  k ) `  w )  /  i ]. a  e.  (
t  e.  v  |->  (
iota_ y  e.  ( Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) )
5719, 48cfv 5255 . . . . . . . 8  class  ( Base `  u )
5856, 11, 57wsbc 2991 . . . . . . 7  wff  [. ( Base `  u )  / 
v ]. [. ( (HDMap1 `  k ) `  w
)  /  i ]. a  e.  ( t  e.  v  |->  ( iota_ y  e.  ( Base `  (
(LCDual `  k ) `  w ) ) A. z  e.  v  ( -.  z  e.  (
( ( LSpan `  u
) `  { e } )  u.  (
( LSpan `  u ) `  { t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) )
59 cdvh 31268 . . . . . . . . 9  class  DVecH
605, 59cfv 5255 . . . . . . . 8  class  ( DVecH `  k )
6131, 60cfv 5255 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
6258, 18, 61wsbc 2991 . . . . . 6  wff  [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) )
63 cid 4304 . . . . . . . 8  class  _I
645, 48cfv 5255 . . . . . . . 8  class  ( Base `  k )
6563, 64cres 4691 . . . . . . 7  class  (  _I  |`  ( Base `  k
) )
66 cltrn 30290 . . . . . . . . . 10  class  LTrn
675, 66cfv 5255 . . . . . . . . 9  class  ( LTrn `  k )
6831, 67cfv 5255 . . . . . . . 8  class  ( (
LTrn `  k ) `  w )
6963, 68cres 4691 . . . . . . 7  class  (  _I  |`  ( ( LTrn `  k
) `  w )
)
7065, 69cop 3643 . . . . . 6  class  <. (  _I  |`  ( Base `  k
) ) ,  (  _I  |`  ( ( LTrn `  k ) `  w ) ) >.
7162, 15, 70wsbc 2991 . . . . 5  wff  [. <. (  _I  |`  ( Base `  k ) ) ,  (  _I  |`  (
( LTrn `  k ) `  w ) ) >.  /  e ]. [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) )
7271, 8cab 2269 . . . 4  class  { a  |  [. <. (  _I  |`  ( Base `  k
) ) ,  (  _I  |`  ( ( LTrn `  k ) `  w ) ) >.  /  e ]. [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) ) }
734, 7, 72cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  { a  | 
[. <. (  _I  |`  ( Base `  k ) ) ,  (  _I  |`  (
( LTrn `  k ) `  w ) ) >.  /  e ]. [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) ) } )
742, 3, 73cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  { a  | 
[. <. (  _I  |`  ( Base `  k ) ) ,  (  _I  |`  (
( LTrn `  k ) `  w ) ) >.  /  e ]. [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) ) } ) )
751, 74wceq 1623 1  wff HDMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. <. (  _I  |`  ( Base `  k
) ) ,  (  _I  |`  ( ( LTrn `  k ) `  w ) ) >.  /  e ]. [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( (HDMap1 `  k
) `  w )  /  i ]. a  e.  ( t  e.  v 
|->  ( iota_ y  e.  (
Base `  ( (LCDual `  k ) `  w
) ) A. z  e.  v  ( -.  z  e.  ( (
( LSpan `  u ) `  { e } )  u.  ( ( LSpan `  u ) `  {
t } ) )  ->  y  =  ( i `  <. z ,  ( i `  <. e ,  ( ( (HVMap `  k ) `  w ) `  e
) ,  z >.
) ,  t >.
) ) ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  hdmapffval  32019
  Copyright terms: Public domain W3C validator