Definition df-lkr 36226

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.)

Assertion

Ref	Expression
df-lkr	⊢ LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))

Distinct variable group:   𝑤,𝑓

Detailed syntax breakdown of Definition df-lkr

Step	Hyp	Ref	Expression
1		clk 36225	. 2 class LKer
2		vw	. . 3 setvar 𝑤
3		cvv 3497	. . 3 class V
4		vf	. . . 4 setvar 𝑓
5	2	cv 1535	. . . . 5 class 𝑤
6		clfn 36197	. . . . 5 class LFnl
7	5, 6	cfv 6358	. . . 4 class (LFnl‘𝑤)
8	4	cv 1535	. . . . . 6 class 𝑓
9	8	ccnv 5557	. . . . 5 class ◡𝑓
10		csca 16571	. . . . . . . 8 class Scalar
11	5, 10	cfv 6358	. . . . . . 7 class (Scalar‘𝑤)
12		c0g 16716	. . . . . . 7 class 0g
13	11, 12	cfv 6358	. . . . . 6 class (0g‘(Scalar‘𝑤))
14	13	csn 4570	. . . . 5 class {(0g‘(Scalar‘𝑤))}
15	9, 14	cima 5561	. . . 4 class (◡𝑓 “ {(0g‘(Scalar‘𝑤))})
16	4, 7, 15	cmpt 5149	. . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))}))
17	2, 3, 16	cmpt 5149	. 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))
18	1, 17	wceq 1536	1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))

This definition is referenced by:  lkrfval  36227