Definition df-lkr 34373

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

Step	Hyp	Ref	Expression
1		clk 34372	. 2 class LKer
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vf	. . . 4 setvar f
5	2	cv 1482	. . . . 5 class w
6		clfn 34344	. . . . 5 class LFnl
7	5, 6	cfv 5888	. . . 4 class (LFnl ` w )
8	4	cv 1482	. . . . . 6 class f
9	8	ccnv 5113	. . . . 5 class `' f
10		csca 15944	. . . . . . . 8 class Scalar
11	5, 10	cfv 5888	. . . . . . 7 class (Scalar ` w )
12		c0g 16100	. . . . . . 7 class 0g
13	11, 12	cfv 5888	. . . . . 6 class ( 0g ` (Scalar ` w ) )
14	13	csn 4177	. . . . 5 class { ( 0g ` (Scalar ` w ) ) }
15	9, 14	cima 5117	. . . 4 class ( `' f " { ( 0g ` (Scalar ` w ) ) } )
16	4, 7, 15	cmpt 4729	. . 3 class ( f e. (LFnl ` w ) |-> ( `' f " { ( 0g ` (Scalar ` w ) ) } ) )
17	2, 3, 16	cmpt 4729	. 2 class ( w e. _V |-> ( f e. (LFnl ` w ) |-> ( `' f " { ( 0g ` (Scalar ` w ) ) } ) ) )
18	1, 17	wceq 1483	1 wff LKer = ( w e. _V |-> ( f e. (LFnl ` w ) |-> ( `' f " { ( 0g ` (Scalar ` w ) ) } ) ) )

This definition is referenced by:  lkrfval  34374