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	$$⊢\mathrm{LKer}=\left(w\in \mathrm{V}⟼\left(f\in \mathrm{LFnl}\left(w\right)⟼f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clk	$$class\mathrm{LKer}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		clfn	$$class\mathrm{LFnl}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class\mathrm{LFnl}\left(w\right)$$
7	3	cv	$$setvarf$$
8	7	ccnv	$$class{f}^{-1}$$
9		c0g	$$class{0}_{𝑔}$$
10		csca	$$class\mathrm{Scalar}$$
11	5 10	cfv	$$class\mathrm{Scalar}\left(w\right)$$
12	11 9	cfv	$$class{0}_{\mathrm{Scalar}\left(w\right)}$$
13	12	csn	$$class\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}$$
14	8 13	cima	$$class{f}^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]$$
15	3 6 14	cmpt	$$class\left(f\in \mathrm{LFnl}\left(w\right)⟼f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]\right)$$
16	1 2 15	cmpt	$$class\left(w\in \mathrm{V}⟼\left(f\in \mathrm{LFnl}\left(w\right)⟼f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]\right)\right)$$
17	0 16	wceq	$$wff\mathrm{LKer}=\left(w\in \mathrm{V}⟼\left(f\in \mathrm{LFnl}\left(w\right)⟼f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]\right)\right)$$