This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → W ∈ LMod
lkrssv.g ⊢ φ → G ∈ F
Assertion lkrssv ⊢ φ → K ⁡ G ⊆ 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 ⊢ φ → W ∈ LMod
5 lkrssv.g ⊢ φ → G ∈ F
6 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
7 2 3 6 lkrlss ⊢ W ∈ LMod ∧ G ∈ F → K ⁡ G ∈ LSubSp ⁡ W
8 4 5 7 syl2anc ⊢ φ → K ⁡ G ∈ LSubSp ⁡ W
9 1 6 lssss ⊢ K ⁡ G ∈ LSubSp ⁡ W → K ⁡ G ⊆ V
10 8 9 syl ⊢ φ → K ⁡ G ⊆ V