Definition df-lkr

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)

	Ref	Expression
Assertion	df-lkr	|- LKer = ( w e. _V |-> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clk	|- LKer
1		vw	|- w
2		cvv	|- _V
3		vf	|- f
4		clfn	|- LFnl
5	1	cv	|- w
6	5 4	cfv	|- ( LFnl ` w )
7	3	cv	|- f
8	7	ccnv	|- `' f
9		c0g	|- 0g
10		csca	|- Scalar
11	5 10	cfv	|- ( Scalar ` w )
12	11 9	cfv	|- ( 0g ` ( Scalar ` w ) )
13	12	csn	|- { ( 0g ` ( Scalar ` w ) ) }
14	8 13	cima	|- ( `' f " { ( 0g ` ( Scalar ` w ) ) } )
15	3 6 14	cmpt	|- ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) )
16	1 2 15	cmpt	|- ( w e. _V |-> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) )
17	0 16	wceq	|- LKer = ( w e. _V |-> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) )