Definition df-lkr 39087

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 39086	. 2 class LKer
2		vw	. . 3 setvar 𝑤
3		cvv 3480	. . 3 class V
4		vf	. . . 4 setvar 𝑓
5	2	cv 1539	. . . . 5 class 𝑤
6		clfn 39058	. . . . 5 class LFnl
7	5, 6	cfv 6561	. . . 4 class (LFnl‘𝑤)
8	4	cv 1539	. . . . . 6 class 𝑓
9	8	ccnv 5684	. . . . 5 class ◡𝑓
10		csca 17300	. . . . . . . 8 class Scalar
11	5, 10	cfv 6561	. . . . . . 7 class (Scalar‘𝑤)
12		c0g 17484	. . . . . . 7 class 0g
13	11, 12	cfv 6561	. . . . . 6 class (0g‘(Scalar‘𝑤))
14	13	csn 4626	. . . . 5 class {(0g‘(Scalar‘𝑤))}
15	9, 14	cima 5688	. . . 4 class (◡𝑓 “ {(0g‘(Scalar‘𝑤))})
16	4, 7, 15	cmpt 5225	. . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))}))
17	2, 3, 16	cmpt 5225	. 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))
18	1, 17	wceq 1540	1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))})))

This definition is referenced by:  lkrfval  39088