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

Definition df-lkr 29276
Description: Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014.)
Assertion
Ref Expression
df-lkr  |- LKer  =  ( w  e.  _V  |->  ( f  e.  (LFnl `  w )  |->  ( `' f " { ( 0g `  (Scalar `  w ) ) } ) ) )
Distinct variable group:    w, f

Detailed syntax breakdown of Definition df-lkr
StepHypRef Expression
1 clk 29275 . 2  class LKer
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vf . . . 4  set  f
52cv 1622 . . . . 5  class  w
6 clfn 29247 . . . . 5  class LFnl
75, 6cfv 5255 . . . 4  class  (LFnl `  w )
84cv 1622 . . . . . 6  class  f
98ccnv 4688 . . . . 5  class  `' f
10 csca 13211 . . . . . . . 8  class Scalar
115, 10cfv 5255 . . . . . . 7  class  (Scalar `  w )
12 c0g 13400 . . . . . . 7  class  0g
1311, 12cfv 5255 . . . . . 6  class  ( 0g
`  (Scalar `  w )
)
1413csn 3640 . . . . 5  class  { ( 0g `  (Scalar `  w ) ) }
159, 14cima 4692 . . . 4  class  ( `' f " { ( 0g `  (Scalar `  w ) ) } )
164, 7, 15cmpt 4077 . . 3  class  ( f  e.  (LFnl `  w
)  |->  ( `' f
" { ( 0g
`  (Scalar `  w )
) } ) )
172, 3, 16cmpt 4077 . 2  class  ( w  e.  _V  |->  ( f  e.  (LFnl `  w
)  |->  ( `' f
" { ( 0g
`  (Scalar `  w )
) } ) ) )
181, 17wceq 1623 1  wff LKer  =  ( w  e.  _V  |->  ( f  e.  (LFnl `  w )  |->  ( `' f " { ( 0g `  (Scalar `  w ) ) } ) ) )
Colors of variables: wff set class
This definition is referenced by:  lkrfval  29277
  Copyright terms: Public domain W3C validator