Theorem lkrcl

Description: A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lkrcl.v	|- V = ( Base ` W )
	lkrcl.f	|- F = ( LFnl ` W )
	lkrcl.k	|- K = ( LKer ` W )
Assertion	lkrcl	|- ( ( W e. Y /\ G e. F /\ X e. ( K ` G ) ) -> X e. V )

Proof

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