Users' Mathboxes 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 33853
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 33852 . 2 class LKer
2 vw . . 3 setvar 𝑤
3 cvv 3186 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1479 . . . . 5 class 𝑤
6 clfn 33824 . . . . 5 class LFnl
75, 6cfv 5847 . . . 4 class (LFnl‘𝑤)
84cv 1479 . . . . . 6 class 𝑓
98ccnv 5073 . . . . 5 class 𝑓
10 csca 15865 . . . . . . . 8 class Scalar
115, 10cfv 5847 . . . . . . 7 class (Scalar‘𝑤)
12 c0g 16021 . . . . . . 7 class 0g
1311, 12cfv 5847 . . . . . 6 class (0g‘(Scalar‘𝑤))
1413csn 4148 . . . . 5 class {(0g‘(Scalar‘𝑤))}
159, 14cima 5077 . . . 4 class (𝑓 “ {(0g‘(Scalar‘𝑤))})
164, 7, 15cmpt 4673 . . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))}))
172, 3, 16cmpt 4673 . 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
181, 17wceq 1480 1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
Colors of variables: wff setvar class
This definition is referenced by:  lkrfval  33854
  Copyright terms: Public domain W3C validator