Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lkr Structured version   Visualization version   GIF version

Definition df-lkr 34894
 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
StepHypRef Expression
1 clk 34893 . 2 class LKer
2 vw . . 3 setvar 𝑤
3 cvv 3340 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1631 . . . . 5 class 𝑤
6 clfn 34865 . . . . 5 class LFnl
75, 6cfv 6049 . . . 4 class (LFnl‘𝑤)
84cv 1631 . . . . . 6 class 𝑓
98ccnv 5265 . . . . 5 class 𝑓
10 csca 16166 . . . . . . . 8 class Scalar
115, 10cfv 6049 . . . . . . 7 class (Scalar‘𝑤)
12 c0g 16322 . . . . . . 7 class 0g
1311, 12cfv 6049 . . . . . 6 class (0g‘(Scalar‘𝑤))
1413csn 4321 . . . . 5 class {(0g‘(Scalar‘𝑤))}
159, 14cima 5269 . . . 4 class (𝑓 “ {(0g‘(Scalar‘𝑤))})
164, 7, 15cmpt 4881 . . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))}))
172, 3, 16cmpt 4881 . 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
181, 17wceq 1632 1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
 Colors of variables: wff setvar class This definition is referenced by:  lkrfval  34895
 Copyright terms: Public domain W3C validator