Theorem lkrval2

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014)

	Ref	Expression
Hypotheses	lkrfval2.v	|- V = ( Base ` W )
	lkrfval2.d	|- D = ( Scalar ` W )
	lkrfval2.o	|- .0. = ( 0g ` D )
	lkrfval2.f	|- F = ( LFnl ` W )
	lkrfval2.k	|- K = ( LKer ` W )
Assertion	lkrval2	|- ( ( W e. X /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } )

Proof

Step	Hyp	Ref	Expression
1		lkrfval2.v	|- V = ( Base ` W )
2		lkrfval2.d	|- D = ( Scalar ` W )
3		lkrfval2.o	|- .0. = ( 0g ` D )
4		lkrfval2.f	|- F = ( LFnl ` W )
5		lkrfval2.k	|- K = ( LKer ` W )
6		elex	|- ( W e. X -> W e. _V )
7	1 2 3 4 5	ellkr	|- ( ( W e. _V /\ G e. F ) -> ( x e. ( K ` G ) <-> ( x e. V /\ ( G ` x ) = .0. ) ) )
8	7	abbi2dv	|- ( ( W e. _V /\ G e. F ) -> ( K ` G ) = { x | ( x e. V /\ ( G ` x ) = .0. ) } )
9		df-rab	|- { x e. V | ( G ` x ) = .0. } = { x | ( x e. V /\ ( G ` x ) = .0. ) }
10	8 9	eqtr4di	|- ( ( W e. _V /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } )
11	6 10	sylan	|- ( ( W e. X /\ G e. F ) -> ( K ` G ) = { x e. V | ( G ` x ) = .0. } )