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

Definition df-hvmap 31947
Description: Extend class notation with a map from each nonzero vector 
x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier e.g. lcf1o 31741, dochfl1 31666- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)
Assertion
Ref Expression
df-hvmap  |- HVMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ( ( Base `  ( ( DVecH `  k
) `  w )
)  \  { ( 0g `  ( ( DVecH `  k ) `  w
) ) } ) 
|->  ( v  e.  (
Base `  ( ( DVecH `  k ) `  w ) )  |->  (
iota_ j  e.  ( Base `  (Scalar `  (
( DVecH `  k ) `  w ) ) ) E. t  e.  ( ( ( ocH `  k
) `  w ) `  { x } ) v  =  ( t ( +g  `  (
( DVecH `  k ) `  w ) ) ( j ( .s `  ( ( DVecH `  k
) `  w )
) x ) ) ) ) ) ) )
Distinct variable group:    w, k, x, v, j, t

Detailed syntax breakdown of Definition df-hvmap
StepHypRef Expression
1 chvm 31946 . 2  class HVMap
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 vx . . . . 5  set  x
94cv 1622 . . . . . . . 8  class  w
10 cdvh 31268 . . . . . . . . 9  class  DVecH
115, 10cfv 5255 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5255 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 13148 . . . . . . 7  class  Base
1412, 13cfv 5255 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
15 c0g 13400 . . . . . . . 8  class  0g
1612, 15cfv 5255 . . . . . . 7  class  ( 0g
`  ( ( DVecH `  k ) `  w
) )
1716csn 3640 . . . . . 6  class  { ( 0g `  ( (
DVecH `  k ) `  w ) ) }
1814, 17cdif 3149 . . . . 5  class  ( (
Base `  ( ( DVecH `  k ) `  w ) )  \  { ( 0g `  ( ( DVecH `  k
) `  w )
) } )
19 vv . . . . . 6  set  v
2019cv 1622 . . . . . . . . 9  class  v
21 vt . . . . . . . . . . 11  set  t
2221cv 1622 . . . . . . . . . 10  class  t
23 vj . . . . . . . . . . . 12  set  j
2423cv 1622 . . . . . . . . . . 11  class  j
258cv 1622 . . . . . . . . . . 11  class  x
26 cvsca 13212 . . . . . . . . . . . 12  class  .s
2712, 26cfv 5255 . . . . . . . . . . 11  class  ( .s
`  ( ( DVecH `  k ) `  w
) )
2824, 25, 27co 5858 . . . . . . . . . 10  class  ( j ( .s `  (
( DVecH `  k ) `  w ) ) x )
29 cplusg 13208 . . . . . . . . . . 11  class  +g
3012, 29cfv 5255 . . . . . . . . . 10  class  ( +g  `  ( ( DVecH `  k
) `  w )
)
3122, 28, 30co 5858 . . . . . . . . 9  class  ( t ( +g  `  (
( DVecH `  k ) `  w ) ) ( j ( .s `  ( ( DVecH `  k
) `  w )
) x ) )
3220, 31wceq 1623 . . . . . . . 8  wff  v  =  ( t ( +g  `  ( ( DVecH `  k
) `  w )
) ( j ( .s `  ( (
DVecH `  k ) `  w ) ) x ) )
3325csn 3640 . . . . . . . . 9  class  { x }
34 coch 31537 . . . . . . . . . . 11  class  ocH
355, 34cfv 5255 . . . . . . . . . 10  class  ( ocH `  k )
369, 35cfv 5255 . . . . . . . . 9  class  ( ( ocH `  k ) `
 w )
3733, 36cfv 5255 . . . . . . . 8  class  ( ( ( ocH `  k
) `  w ) `  { x } )
3832, 21, 37wrex 2544 . . . . . . 7  wff  E. t  e.  ( ( ( ocH `  k ) `  w
) `  { x } ) v  =  ( t ( +g  `  ( ( DVecH `  k
) `  w )
) ( j ( .s `  ( (
DVecH `  k ) `  w ) ) x ) )
39 csca 13211 . . . . . . . . 9  class Scalar
4012, 39cfv 5255 . . . . . . . 8  class  (Scalar `  ( ( DVecH `  k
) `  w )
)
4140, 13cfv 5255 . . . . . . 7  class  ( Base `  (Scalar `  ( ( DVecH `  k ) `  w ) ) )
4238, 23, 41crio 6297 . . . . . 6  class  ( iota_ j  e.  ( Base `  (Scalar `  ( ( DVecH `  k
) `  w )
) ) E. t  e.  ( ( ( ocH `  k ) `  w
) `  { x } ) v  =  ( t ( +g  `  ( ( DVecH `  k
) `  w )
) ( j ( .s `  ( (
DVecH `  k ) `  w ) ) x ) ) )
4319, 14, 42cmpt 4077 . . . . 5  class  ( v  e.  ( Base `  (
( DVecH `  k ) `  w ) )  |->  (
iota_ j  e.  ( Base `  (Scalar `  (
( DVecH `  k ) `  w ) ) ) E. t  e.  ( ( ( ocH `  k
) `  w ) `  { x } ) v  =  ( t ( +g  `  (
( DVecH `  k ) `  w ) ) ( j ( .s `  ( ( DVecH `  k
) `  w )
) x ) ) ) )
448, 18, 43cmpt 4077 . . . 4  class  ( x  e.  ( ( Base `  ( ( DVecH `  k
) `  w )
)  \  { ( 0g `  ( ( DVecH `  k ) `  w
) ) } ) 
|->  ( v  e.  (
Base `  ( ( DVecH `  k ) `  w ) )  |->  (
iota_ j  e.  ( Base `  (Scalar `  (
( DVecH `  k ) `  w ) ) ) E. t  e.  ( ( ( ocH `  k
) `  w ) `  { x } ) v  =  ( t ( +g  `  (
( DVecH `  k ) `  w ) ) ( j ( .s `  ( ( DVecH `  k
) `  w )
) x ) ) ) ) )
454, 7, 44cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e.  ( ( Base `  (
( DVecH `  k ) `  w ) )  \  { ( 0g `  ( ( DVecH `  k
) `  w )
) } )  |->  ( v  e.  ( Base `  ( ( DVecH `  k
) `  w )
)  |->  ( iota_ j  e.  ( Base `  (Scalar `  ( ( DVecH `  k
) `  w )
) ) E. t  e.  ( ( ( ocH `  k ) `  w
) `  { x } ) v  =  ( t ( +g  `  ( ( DVecH `  k
) `  w )
) ( j ( .s `  ( (
DVecH `  k ) `  w ) ) x ) ) ) ) ) )
462, 3, 45cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e.  ( ( Base `  (
( DVecH `  k ) `  w ) )  \  { ( 0g `  ( ( DVecH `  k
) `  w )
) } )  |->  ( v  e.  ( Base `  ( ( DVecH `  k
) `  w )
)  |->  ( iota_ j  e.  ( Base `  (Scalar `  ( ( DVecH `  k
) `  w )
) ) E. t  e.  ( ( ( ocH `  k ) `  w
) `  { x } ) v  =  ( t ( +g  `  ( ( DVecH `  k
) `  w )
) ( j ( .s `  ( (
DVecH `  k ) `  w ) ) x ) ) ) ) ) ) )
471, 46wceq 1623 1  wff HVMap  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ( ( Base `  ( ( DVecH `  k
) `  w )
)  \  { ( 0g `  ( ( DVecH `  k ) `  w
) ) } ) 
|->  ( v  e.  (
Base `  ( ( DVecH `  k ) `  w ) )  |->  (
iota_ j  e.  ( Base `  (Scalar `  (
( DVecH `  k ) `  w ) ) ) E. t  e.  ( ( ( ocH `  k
) `  w ) `  { x } ) v  =  ( t ( +g  `  (
( DVecH `  k ) `  w ) ) ( j ( .s `  ( ( DVecH `  k
) `  w )
) x ) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  hvmapffval  31948
  Copyright terms: Public domain W3C validator