# 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 ${⊢}\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 ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vf ${setvar}{f}$
4 clfn ${class}\mathrm{LFnl}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}\mathrm{LFnl}\left({w}\right)$
7 3 cv ${setvar}{f}$
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)$