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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrssv.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrssv.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lkrssv.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lkrssv.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lkrssv	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lkrssv.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrssv.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
3		lkrssv.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
4		lkrssv.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lkrssv.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
6		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
7	2 3 6	lkrlss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
8	4 5 7	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
9	1 6	lssss	⊢ ( ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) → ( 𝐾 ‘ 𝐺 ) ⊆ 𝑉 )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ 𝑉 )