Theorem lkrf0

Description: The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lkrf0.d	|- D = ( Scalar ` W )
	lkrf0.o	|- .0. = ( 0g ` D )
	lkrf0.f	|- F = ( LFnl ` W )
	lkrf0.k	|- K = ( LKer ` W )
Assertion	lkrf0	|- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> ( G ` X ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		lkrf0.d	|- D = ( Scalar ` W )
2		lkrf0.o	|- .0. = ( 0g ` D )
3		lkrf0.f	|- F = ( LFnl ` W )
4		lkrf0.k	|- K = ( LKer ` W )
5		eqid	|- ( Base ` W ) = ( Base ` W )
6	5 1 2 3 4	ellkr	|- ( ( W e. Y /\ G e. F ) -> ( X e. ( K ` G ) <-> ( X e. ( Base ` W ) /\ ( G ` X ) = .0. ) ) )
7	6	simplbda	|- ( ( ( W e. Y /\ G e. F ) /\ X e. ( K ` G ) ) -> ( G ` X ) = .0. )
8	7	3impa	|- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> ( G ` X ) = .0. )