Definition df-lkr 33391

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 33390	. 2 class LKer
2		vw	. . 3 setvar 𝑤
3		cvv 3173	. . 3 class V
4		vf	. . . 4 setvar 𝑓
5	2	cv 1474	. . . . 5 class 𝑤
6		clfn 33362	. . . . 5 class LFnl
7	5, 6	cfv 5804	. . . 4 class (LFnl‘𝑤)
8	4	cv 1474	. . . . . 6 class 𝑓
9	8	ccnv 5037	. . . . 5 class ◡𝑓
10		csca 15771	. . . . . . . 8 class Scalar
11	5, 10	cfv 5804	. . . . . . 7 class (Scalar‘𝑤)
12		c0g 15923	. . . . . . 7 class 0g
13	11, 12	cfv 5804	. . . . . 6 class (0g‘(Scalar‘𝑤))
14	13	csn 4125	. . . . 5 class {(0g‘(Scalar‘𝑤))}
15	9, 14	cima 5041	. . . 4 class (◡𝑓 “ {(0g‘(Scalar‘𝑤))})
16	4, 7, 15	cmpt 4643	. . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))}))
17	2, 3, 16	cmpt 4643	. 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))
18	1, 17	wceq 1475	1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))

This definition is referenced by:  lkrfval  33392