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

Definition df-hdmap1 32606
Description: Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 32609 description for more details. (Contributed by NM, 14-May-2015.)
Assertion
Ref Expression
df-hdmap1  |- HDMap1  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. ( (
DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( LSpan `  u )  /  n ]. [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) ) } ) )
Distinct variable group:    a, c, d, h, j, k, m, n, u, v, w, x

Detailed syntax breakdown of Definition df-hdmap1
StepHypRef Expression
1 chdma1 32604 . 2  class HDMap1
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1631 . . . . 5  class  k
6 clh 30795 . . . . 5  class  LHyp
75, 6cfv 5271 . . . 4  class  ( LHyp `  k )
8 va . . . . . . . . . . . . . 14  set  a
98cv 1631 . . . . . . . . . . . . 13  class  a
10 vx . . . . . . . . . . . . . 14  set  x
11 vv . . . . . . . . . . . . . . . . 17  set  v
1211cv 1631 . . . . . . . . . . . . . . . 16  class  v
13 vd . . . . . . . . . . . . . . . . 17  set  d
1413cv 1631 . . . . . . . . . . . . . . . 16  class  d
1512, 14cxp 4703 . . . . . . . . . . . . . . 15  class  ( v  X.  d )
1615, 12cxp 4703 . . . . . . . . . . . . . 14  class  ( ( v  X.  d )  X.  v )
1710cv 1631 . . . . . . . . . . . . . . . . 17  class  x
18 c2nd 6137 . . . . . . . . . . . . . . . . 17  class  2nd
1917, 18cfv 5271 . . . . . . . . . . . . . . . 16  class  ( 2nd `  x )
20 vu . . . . . . . . . . . . . . . . . 18  set  u
2120cv 1631 . . . . . . . . . . . . . . . . 17  class  u
22 c0g 13416 . . . . . . . . . . . . . . . . 17  class  0g
2321, 22cfv 5271 . . . . . . . . . . . . . . . 16  class  ( 0g
`  u )
2419, 23wceq 1632 . . . . . . . . . . . . . . 15  wff  ( 2nd `  x )  =  ( 0g `  u )
25 vc . . . . . . . . . . . . . . . . 17  set  c
2625cv 1631 . . . . . . . . . . . . . . . 16  class  c
2726, 22cfv 5271 . . . . . . . . . . . . . . 15  class  ( 0g
`  c )
2819csn 3653 . . . . . . . . . . . . . . . . . . . 20  class  { ( 2nd `  x ) }
29 vn . . . . . . . . . . . . . . . . . . . . 21  set  n
3029cv 1631 . . . . . . . . . . . . . . . . . . . 20  class  n
3128, 30cfv 5271 . . . . . . . . . . . . . . . . . . 19  class  ( n `
 { ( 2nd `  x ) } )
32 vm . . . . . . . . . . . . . . . . . . . 20  set  m
3332cv 1631 . . . . . . . . . . . . . . . . . . 19  class  m
3431, 33cfv 5271 . . . . . . . . . . . . . . . . . 18  class  ( m `
 ( n `  { ( 2nd `  x
) } ) )
35 vh . . . . . . . . . . . . . . . . . . . . 21  set  h
3635cv 1631 . . . . . . . . . . . . . . . . . . . 20  class  h
3736csn 3653 . . . . . . . . . . . . . . . . . . 19  class  { h }
38 vj . . . . . . . . . . . . . . . . . . . 20  set  j
3938cv 1631 . . . . . . . . . . . . . . . . . . 19  class  j
4037, 39cfv 5271 . . . . . . . . . . . . . . . . . 18  class  ( j `
 { h }
)
4134, 40wceq 1632 . . . . . . . . . . . . . . . . 17  wff  ( m `
 ( n `  { ( 2nd `  x
) } ) )  =  ( j `  { h } )
42 c1st 6136 . . . . . . . . . . . . . . . . . . . . . . . 24  class  1st
4317, 42cfv 5271 . . . . . . . . . . . . . . . . . . . . . . 23  class  ( 1st `  x )
4443, 42cfv 5271 . . . . . . . . . . . . . . . . . . . . . 22  class  ( 1st `  ( 1st `  x
) )
45 csg 14381 . . . . . . . . . . . . . . . . . . . . . . 23  class  -g
4621, 45cfv 5271 . . . . . . . . . . . . . . . . . . . . . 22  class  ( -g `  u )
4744, 19, 46co 5874 . . . . . . . . . . . . . . . . . . . . 21  class  ( ( 1st `  ( 1st `  x ) ) (
-g `  u )
( 2nd `  x
) )
4847csn 3653 . . . . . . . . . . . . . . . . . . . 20  class  { ( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) }
4948, 30cfv 5271 . . . . . . . . . . . . . . . . . . 19  class  ( n `
 { ( ( 1st `  ( 1st `  x ) ) (
-g `  u )
( 2nd `  x
) ) } )
5049, 33cfv 5271 . . . . . . . . . . . . . . . . . 18  class  ( m `
 ( n `  { ( ( 1st `  ( 1st `  x
) ) ( -g `  u ) ( 2nd `  x ) ) } ) )
5143, 18cfv 5271 . . . . . . . . . . . . . . . . . . . . 21  class  ( 2nd `  ( 1st `  x
) )
5226, 45cfv 5271 . . . . . . . . . . . . . . . . . . . . 21  class  ( -g `  c )
5351, 36, 52co 5874 . . . . . . . . . . . . . . . . . . . 20  class  ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h )
5453csn 3653 . . . . . . . . . . . . . . . . . . 19  class  { ( ( 2nd `  ( 1st `  x ) ) ( -g `  c
) h ) }
5554, 39cfv 5271 . . . . . . . . . . . . . . . . . 18  class  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } )
5650, 55wceq 1632 . . . . . . . . . . . . . . . . 17  wff  ( m `
 ( n `  { ( ( 1st `  ( 1st `  x
) ) ( -g `  u ) ( 2nd `  x ) ) } ) )  =  ( j `  { ( ( 2nd `  ( 1st `  x ) ) ( -g `  c
) h ) } )
5741, 56wa 358 . . . . . . . . . . . . . . . 16  wff  ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) )
5857, 35, 14crio 6313 . . . . . . . . . . . . . . 15  class  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) )
5924, 27, 58cif 3578 . . . . . . . . . . . . . 14  class  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) )
6010, 16, 59cmpt 4093 . . . . . . . . . . . . 13  class  ( x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
619, 60wcel 1696 . . . . . . . . . . . 12  wff  a  e.  ( x  e.  ( ( v  X.  d
)  X.  v ) 
|->  if ( ( 2nd `  x )  =  ( 0g `  u ) ,  ( 0g `  c ) ,  (
iota_ h  e.  d
( ( m `  ( n `  {
( 2nd `  x
) } ) )  =  ( j `  { h } )  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
624cv 1631 . . . . . . . . . . . . 13  class  w
63 cmpd 32436 . . . . . . . . . . . . . 14  class mapd
645, 63cfv 5271 . . . . . . . . . . . . 13  class  (mapd `  k )
6562, 64cfv 5271 . . . . . . . . . . . 12  class  ( (mapd `  k ) `  w
)
6661, 32, 65wsbc 3004 . . . . . . . . . . 11  wff  [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
67 clspn 15744 . . . . . . . . . . . 12  class  LSpan
6826, 67cfv 5271 . . . . . . . . . . 11  class  ( LSpan `  c )
6966, 38, 68wsbc 3004 . . . . . . . . . 10  wff  [. ( LSpan `  c )  / 
j ]. [. ( (mapd `  k ) `  w
)  /  m ]. a  e.  ( x  e.  ( ( v  X.  d )  X.  v
)  |->  if ( ( 2nd `  x )  =  ( 0g `  u ) ,  ( 0g `  c ) ,  ( iota_ h  e.  d ( ( m `
 ( n `  { ( 2nd `  x
) } ) )  =  ( j `  { h } )  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
70 cbs 13164 . . . . . . . . . . 11  class  Base
7126, 70cfv 5271 . . . . . . . . . 10  class  ( Base `  c )
7269, 13, 71wsbc 3004 . . . . . . . . 9  wff  [. ( Base `  c )  / 
d ]. [. ( LSpan `  c )  /  j ]. [. ( (mapd `  k ) `  w
)  /  m ]. a  e.  ( x  e.  ( ( v  X.  d )  X.  v
)  |->  if ( ( 2nd `  x )  =  ( 0g `  u ) ,  ( 0g `  c ) ,  ( iota_ h  e.  d ( ( m `
 ( n `  { ( 2nd `  x
) } ) )  =  ( j `  { h } )  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
73 clcd 32398 . . . . . . . . . . 11  class LCDual
745, 73cfv 5271 . . . . . . . . . 10  class  (LCDual `  k )
7562, 74cfv 5271 . . . . . . . . 9  class  ( (LCDual `  k ) `  w
)
7672, 25, 75wsbc 3004 . . . . . . . 8  wff  [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
7721, 67cfv 5271 . . . . . . . 8  class  ( LSpan `  u )
7876, 29, 77wsbc 3004 . . . . . . 7  wff  [. ( LSpan `  u )  /  n ]. [. ( (LCDual `  k ) `  w
)  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
7921, 70cfv 5271 . . . . . . 7  class  ( Base `  u )
8078, 11, 79wsbc 3004 . . . . . 6  wff  [. ( Base `  u )  / 
v ]. [. ( LSpan `  u )  /  n ]. [. ( (LCDual `  k ) `  w
)  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
81 cdvh 31890 . . . . . . . 8  class  DVecH
825, 81cfv 5271 . . . . . . 7  class  ( DVecH `  k )
8362, 82cfv 5271 . . . . . 6  class  ( (
DVecH `  k ) `  w )
8480, 20, 83wsbc 3004 . . . . 5  wff  [. (
( DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( LSpan `  u )  /  n ]. [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) )
8584, 8cab 2282 . . . 4  class  { a  |  [. ( (
DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( LSpan `  u )  /  n ]. [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) ) }
864, 7, 85cmpt 4093 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  { a  | 
[. ( ( DVecH `  k ) `  w
)  /  u ]. [. ( Base `  u
)  /  v ]. [. ( LSpan `  u )  /  n ]. [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) ) } )
872, 3, 86cmpt 4093 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  { a  | 
[. ( ( DVecH `  k ) `  w
)  /  u ]. [. ( Base `  u
)  /  v ]. [. ( LSpan `  u )  /  n ]. [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) ) } ) )
881, 87wceq 1632 1  wff HDMap1  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { a  |  [. ( (
DVecH `  k ) `  w )  /  u ]. [. ( Base `  u
)  /  v ]. [. ( LSpan `  u )  /  n ]. [. (
(LCDual `  k ) `  w )  /  c ]. [. ( Base `  c
)  /  d ]. [. ( LSpan `  c )  /  j ]. [. (
(mapd `  k ) `  w )  /  m ]. a  e.  (
x  e.  ( ( v  X.  d )  X.  v )  |->  if ( ( 2nd `  x
)  =  ( 0g
`  u ) ,  ( 0g `  c
) ,  ( iota_ h  e.  d ( ( m `  ( n `
 { ( 2nd `  x ) } ) )  =  ( j `
 { h }
)  /\  ( m `  ( n `  {
( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) } ) )  =  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } ) ) ) ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  hdmap1ffval  32608
  Copyright terms: Public domain W3C validator