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

Definition df-lkr 29821
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 29820 . 2  class LKer
2 vw . . 3  set  w
3 cvv 2948 . . 3  class  _V
4 vf . . . 4  set  f
52cv 1651 . . . . 5  class  w
6 clfn 29792 . . . . 5  class LFnl
75, 6cfv 5446 . . . 4  class  (LFnl `  w )
84cv 1651 . . . . . 6  class  f
98ccnv 4869 . . . . 5  class  `' f
10 csca 13524 . . . . . . . 8  class Scalar
115, 10cfv 5446 . . . . . . 7  class  (Scalar `  w )
12 c0g 13715 . . . . . . 7  class  0g
1311, 12cfv 5446 . . . . . 6  class  ( 0g
`  (Scalar `  w )
)
1413csn 3806 . . . . 5  class  { ( 0g `  (Scalar `  w ) ) }
159, 14cima 4873 . . . 4  class  ( `' f " { ( 0g `  (Scalar `  w ) ) } )
164, 7, 15cmpt 4258 . . 3  class  ( f  e.  (LFnl `  w
)  |->  ( `' f
" { ( 0g
`  (Scalar `  w )
) } ) )
172, 3, 16cmpt 4258 . 2  class  ( w  e.  _V  |->  ( f  e.  (LFnl `  w
)  |->  ( `' f
" { ( 0g
`  (Scalar `  w )
) } ) ) )
181, 17wceq 1652 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  29822
  Copyright terms: Public domain W3C validator