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

Definition df-lcdual 32399
Description: Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 32461. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 32437 using  ( Base `  (
(LCDual `  K ) `  W ) ). (Contributed by NM, 13-Mar-2015.)
Assertion
Ref Expression
df-lcdual  |- LCDual  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( (LDual `  ( ( DVecH `  k
) `  w )
)s 
{ f  e.  (LFnl `  ( ( DVecH `  k
) `  w )
)  |  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f ) } ) ) )
Distinct variable group:    f, k, w

Detailed syntax breakdown of Definition df-lcdual
StepHypRef Expression
1 clcd 32398 . 2  class LCDual
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 )
84cv 1631 . . . . . . 7  class  w
9 cdvh 31890 . . . . . . . 8  class  DVecH
105, 9cfv 5271 . . . . . . 7  class  ( DVecH `  k )
118, 10cfv 5271 . . . . . 6  class  ( (
DVecH `  k ) `  w )
12 cld 29935 . . . . . 6  class LDual
1311, 12cfv 5271 . . . . 5  class  (LDual `  ( ( DVecH `  k
) `  w )
)
14 vf . . . . . . . . . . 11  set  f
1514cv 1631 . . . . . . . . . 10  class  f
16 clk 29897 . . . . . . . . . . 11  class LKer
1711, 16cfv 5271 . . . . . . . . . 10  class  (LKer `  ( ( DVecH `  k
) `  w )
)
1815, 17cfv 5271 . . . . . . . . 9  class  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
19 coch 32159 . . . . . . . . . . 11  class  ocH
205, 19cfv 5271 . . . . . . . . . 10  class  ( ocH `  k )
218, 20cfv 5271 . . . . . . . . 9  class  ( ( ocH `  k ) `
 w )
2218, 21cfv 5271 . . . . . . . 8  class  ( ( ( ocH `  k
) `  w ) `  ( (LKer `  (
( DVecH `  k ) `  w ) ) `  f ) )
2322, 21cfv 5271 . . . . . . 7  class  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )
2423, 18wceq 1632 . . . . . 6  wff  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f )
25 clfn 29869 . . . . . . 7  class LFnl
2611, 25cfv 5271 . . . . . 6  class  (LFnl `  ( ( DVecH `  k
) `  w )
)
2724, 14, 26crab 2560 . . . . 5  class  { f  e.  (LFnl `  (
( DVecH `  k ) `  w ) )  |  ( ( ( ocH `  k ) `  w
) `  ( (
( ocH `  k
) `  w ) `  ( (LKer `  (
( DVecH `  k ) `  w ) ) `  f ) ) )  =  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f ) }
28 cress 13165 . . . . 5  classs
2913, 27, 28co 5874 . . . 4  class  ( (LDual `  ( ( DVecH `  k
) `  w )
)s 
{ f  e.  (LFnl `  ( ( DVecH `  k
) `  w )
)  |  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f ) } )
304, 7, 29cmpt 4093 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( (LDual `  ( ( DVecH `  k
) `  w )
)s 
{ f  e.  (LFnl `  ( ( DVecH `  k
) `  w )
)  |  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f ) } ) )
312, 3, 30cmpt 4093 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( (LDual `  ( ( DVecH `  k
) `  w )
)s 
{ f  e.  (LFnl `  ( ( DVecH `  k
) `  w )
)  |  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f ) } ) ) )
321, 31wceq 1632 1  wff LCDual  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( (LDual `  ( ( DVecH `  k
) `  w )
)s 
{ f  e.  (LFnl `  ( ( DVecH `  k
) `  w )
)  |  ( ( ( ocH `  k
) `  w ) `  ( ( ( ocH `  k ) `  w
) `  ( (LKer `  ( ( DVecH `  k
) `  w )
) `  f )
) )  =  ( (LKer `  ( ( DVecH `  k ) `  w ) ) `  f ) } ) ) )
Colors of variables: wff set class
This definition is referenced by:  lcdfval  32400
  Copyright terms: Public domain W3C validator