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

Metamath Proof Explorer

Definition df-lkr

Description: Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014)

Ref Expression
Assertion df-lkr ⊢ LKer = w ∈ V ⟼ f ∈ LFnl ⁡ w ⟼ f -1 0 Scalar ⁡ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 clk class LKer
1 vw setvar w
2 cvv class V
3 vf setvar f
4 clfn class LFnl
5 1 cv setvar w
6 5 4 cfv class LFnl ⁡ w
7 3 cv setvar f
8 7 ccnv class f -1
9 c0g class 0 𝑔
10 csca class Scalar
11 5 10 cfv class Scalar ⁡ w
12 11 9 cfv class 0 Scalar ⁡ w
13 12 csn class 0 Scalar ⁡ w
14 8 13 cima class f -1 0 Scalar ⁡ w
15 3 6 14 cmpt class f ∈ LFnl ⁡ w ⟼ f -1 0 Scalar ⁡ w
16 1 2 15 cmpt class w ∈ V ⟼ f ∈ LFnl ⁡ w ⟼ f -1 0 Scalar ⁡ w
17 0 16 wceq wff LKer = w ∈ V ⟼ f ∈ LFnl ⁡ w ⟼ f -1 0 Scalar ⁡ w