Theorem lkrfval

Description: The kernel of a functional. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lkrfval.d	|- D = ( Scalar ` W )
	lkrfval.o	|- .0. = ( 0g ` D )
	lkrfval.f	|- F = ( LFnl ` W )
	lkrfval.k	|- K = ( LKer ` W )
Assertion	lkrfval	|- ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lkrfval.d	|- D = ( Scalar ` W )
2		lkrfval.o	|- .0. = ( 0g ` D )
3		lkrfval.f	|- F = ( LFnl ` W )
4		lkrfval.k	|- K = ( LKer ` W )
5		elex	|- ( W e. X -> W e. _V )
6		fveq2	|- ( w = W -> ( LFnl ` w ) = ( LFnl ` W ) )
7	6 3	eqtr4di	|- ( w = W -> ( LFnl ` w ) = F )
8		fveq2	|- ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
9	8 1	eqtr4di	|- ( w = W -> ( Scalar ` w ) = D )
10	9	fveq2d	|- ( w = W -> ( 0g ` ( Scalar ` w ) ) = ( 0g ` D ) )
11	10 2	eqtr4di	|- ( w = W -> ( 0g ` ( Scalar ` w ) ) = .0. )
12	11	sneqd	|- ( w = W -> { ( 0g ` ( Scalar ` w ) ) } = { .0. } )
13	12	imaeq2d	|- ( w = W -> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) = ( `' f " { .0. } ) )
14	7 13	mpteq12dv	|- ( w = W -> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) = ( f e. F |-> ( `' f " { .0. } ) ) )
15		df-lkr	|- LKer = ( w e. _V |-> ( f e. ( LFnl ` w ) |-> ( `' f " { ( 0g ` ( Scalar ` w ) ) } ) ) )
16	14 15 3	mptfvmpt	|- ( W e. _V -> ( LKer ` W ) = ( f e. F |-> ( `' f " { .0. } ) ) )
17	4 16	syl5eq	|- ( W e. _V -> K = ( f e. F |-> ( `' f " { .0. } ) ) )
18	5 17	syl	|- ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) )