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

Definition df-hdmap1 31984
Description: Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 31987 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 31982 . 2  class HDMap1
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 . . . . . . . . . . . . . 14  set  a
98cv 1622 . . . . . . . . . . . . 13  class  a
10 vx . . . . . . . . . . . . . 14  set  x
11 vv . . . . . . . . . . . . . . . . 17  set  v
1211cv 1622 . . . . . . . . . . . . . . . 16  class  v
13 vd . . . . . . . . . . . . . . . . 17  set  d
1413cv 1622 . . . . . . . . . . . . . . . 16  class  d
1512, 14cxp 4687 . . . . . . . . . . . . . . 15  class  ( v  X.  d )
1615, 12cxp 4687 . . . . . . . . . . . . . 14  class  ( ( v  X.  d )  X.  v )
1710cv 1622 . . . . . . . . . . . . . . . . 17  class  x
18 c2nd 6121 . . . . . . . . . . . . . . . . 17  class  2nd
1917, 18cfv 5255 . . . . . . . . . . . . . . . 16  class  ( 2nd `  x )
20 vu . . . . . . . . . . . . . . . . . 18  set  u
2120cv 1622 . . . . . . . . . . . . . . . . 17  class  u
22 c0g 13400 . . . . . . . . . . . . . . . . 17  class  0g
2321, 22cfv 5255 . . . . . . . . . . . . . . . 16  class  ( 0g
`  u )
2419, 23wceq 1623 . . . . . . . . . . . . . . 15  wff  ( 2nd `  x )  =  ( 0g `  u )
25 vc . . . . . . . . . . . . . . . . 17  set  c
2625cv 1622 . . . . . . . . . . . . . . . 16  class  c
2726, 22cfv 5255 . . . . . . . . . . . . . . 15  class  ( 0g
`  c )
2819csn 3640 . . . . . . . . . . . . . . . . . . . 20  class  { ( 2nd `  x ) }
29 vn . . . . . . . . . . . . . . . . . . . . 21  set  n
3029cv 1622 . . . . . . . . . . . . . . . . . . . 20  class  n
3128, 30cfv 5255 . . . . . . . . . . . . . . . . . . 19  class  ( n `
 { ( 2nd `  x ) } )
32 vm . . . . . . . . . . . . . . . . . . . 20  set  m
3332cv 1622 . . . . . . . . . . . . . . . . . . 19  class  m
3431, 33cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( m `
 ( n `  { ( 2nd `  x
) } ) )
35 vh . . . . . . . . . . . . . . . . . . . . 21  set  h
3635cv 1622 . . . . . . . . . . . . . . . . . . . 20  class  h
3736csn 3640 . . . . . . . . . . . . . . . . . . 19  class  { h }
38 vj . . . . . . . . . . . . . . . . . . . 20  set  j
3938cv 1622 . . . . . . . . . . . . . . . . . . 19  class  j
4037, 39cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( j `
 { h }
)
4134, 40wceq 1623 . . . . . . . . . . . . . . . . 17  wff  ( m `
 ( n `  { ( 2nd `  x
) } ) )  =  ( j `  { h } )
42 c1st 6120 . . . . . . . . . . . . . . . . . . . . . . . 24  class  1st
4317, 42cfv 5255 . . . . . . . . . . . . . . . . . . . . . . 23  class  ( 1st `  x )
4443, 42cfv 5255 . . . . . . . . . . . . . . . . . . . . . 22  class  ( 1st `  ( 1st `  x
) )
45 csg 14365 . . . . . . . . . . . . . . . . . . . . . . 23  class  -g
4621, 45cfv 5255 . . . . . . . . . . . . . . . . . . . . . 22  class  ( -g `  u )
4744, 19, 46co 5858 . . . . . . . . . . . . . . . . . . . . 21  class  ( ( 1st `  ( 1st `  x ) ) (
-g `  u )
( 2nd `  x
) )
4847csn 3640 . . . . . . . . . . . . . . . . . . . 20  class  { ( ( 1st `  ( 1st `  x ) ) ( -g `  u
) ( 2nd `  x
) ) }
4948, 30cfv 5255 . . . . . . . . . . . . . . . . . . 19  class  ( n `
 { ( ( 1st `  ( 1st `  x ) ) (
-g `  u )
( 2nd `  x
) ) } )
5049, 33cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( m `
 ( n `  { ( ( 1st `  ( 1st `  x
) ) ( -g `  u ) ( 2nd `  x ) ) } ) )
5143, 18cfv 5255 . . . . . . . . . . . . . . . . . . . . 21  class  ( 2nd `  ( 1st `  x
) )
5226, 45cfv 5255 . . . . . . . . . . . . . . . . . . . . 21  class  ( -g `  c )
5351, 36, 52co 5858 . . . . . . . . . . . . . . . . . . . 20  class  ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h )
5453csn 3640 . . . . . . . . . . . . . . . . . . 19  class  { ( ( 2nd `  ( 1st `  x ) ) ( -g `  c
) h ) }
5554, 39cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( j `
 { ( ( 2nd `  ( 1st `  x ) ) (
-g `  c )
h ) } )
5650, 55wceq 1623 . . . . . . . . . . . . . . . . 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 6297 . . . . . . . . . . . . . . 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 3565 . . . . . . . . . . . . . 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 4077 . . . . . . . . . . . . 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 1684 . . . . . . . . . . . 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 1622 . . . . . . . . . . . . 13  class  w
63 cmpd 31814 . . . . . . . . . . . . . 14  class mapd
645, 63cfv 5255 . . . . . . . . . . . . 13  class  (mapd `  k )
6562, 64cfv 5255 . . . . . . . . . . . 12  class  ( (mapd `  k ) `  w
)
6661, 32, 65wsbc 2991 . . . . . . . . . . 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 15728 . . . . . . . . . . . 12  class  LSpan
6826, 67cfv 5255 . . . . . . . . . . 11  class  ( LSpan `  c )
6966, 38, 68wsbc 2991 . . . . . . . . . 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 13148 . . . . . . . . . . 11  class  Base
7126, 70cfv 5255 . . . . . . . . . 10  class  ( Base `  c )
7269, 13, 71wsbc 2991 . . . . . . . . 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 31776 . . . . . . . . . . 11  class LCDual
745, 73cfv 5255 . . . . . . . . . 10  class  (LCDual `  k )
7562, 74cfv 5255 . . . . . . . . 9  class  ( (LCDual `  k ) `  w
)
7672, 25, 75wsbc 2991 . . . . . . . 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 5255 . . . . . . . 8  class  ( LSpan `  u )
7876, 29, 77wsbc 2991 . . . . . . 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 5255 . . . . . . 7  class  ( Base `  u )
8078, 11, 79wsbc 2991 . . . . . 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 31268 . . . . . . . 8  class  DVecH
825, 81cfv 5255 . . . . . . 7  class  ( DVecH `  k )
8362, 82cfv 5255 . . . . . 6  class  ( (
DVecH `  k ) `  w )
8480, 20, 83wsbc 2991 . . . . 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 2269 . . . 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 4077 . . 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 4077 . 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 1623 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  31986
  Copyright terms: Public domain W3C validator