This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) } ) ) )