Theorem lkrssv

Description: The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015)

	Ref	Expression
Hypotheses	lkrssv.v	|- V = ( Base ` W )
	lkrssv.f	|- F = ( LFnl ` W )
	lkrssv.k	|- K = ( LKer ` W )
	lkrssv.w	|- ( ph -> W e. LMod )
	lkrssv.g	|- ( ph -> G e. F )
Assertion	lkrssv	|- ( ph -> ( K ` G ) C_ V )

Proof

Step	Hyp	Ref	Expression
1		lkrssv.v	|- V = ( Base ` W )
2		lkrssv.f	|- F = ( LFnl ` W )
3		lkrssv.k	|- K = ( LKer ` W )
4		lkrssv.w	|- ( ph -> W e. LMod )
5		lkrssv.g	|- ( ph -> G e. F )
6		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
7	2 3 6	lkrlss	|- ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. ( LSubSp ` W ) )
8	4 5 7	syl2anc	|- ( ph -> ( K ` G ) e. ( LSubSp ` W ) )
9	1 6	lssss	|- ( ( K ` G ) e. ( LSubSp ` W ) -> ( K ` G ) C_ V )
10	8 9	syl	|- ( ph -> ( K ` G ) C_ V )