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

Metamath Proof Explorer

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 ∈ Y ∧ G ∈ F ∧ X ∈ K ⁡ G → X ∈ 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 ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
6 1 4 5 2 3 ellkr ⊢ W ∈ Y ∧ G ∈ F → X ∈ K ⁡ G ↔ X ∈ V ∧ G ⁡ X = 0 Scalar ⁡ W
7 6 simprbda ⊢ W ∈ Y ∧ G ∈ F ∧ X ∈ K ⁡ G → X ∈ V
8 7 3impa ⊢ W ∈ Y ∧ G ∈ F ∧ X ∈ K ⁡ G → X ∈ V