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 36294
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 36293 . 2 class LKer
2 vw . . 3 setvar 𝑤
3 cvv 3480 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1537 . . . . 5 class 𝑤
6 clfn 36265 . . . . 5 class LFnl
75, 6cfv 6344 . . . 4 class (LFnl‘𝑤)
84cv 1537 . . . . . 6 class 𝑓
98ccnv 5542 . . . . 5 class 𝑓
10 csca 16566 . . . . . . . 8 class Scalar
115, 10cfv 6344 . . . . . . 7 class (Scalar‘𝑤)
12 c0g 16711 . . . . . . 7 class 0g
1311, 12cfv 6344 . . . . . 6 class (0g‘(Scalar‘𝑤))
1413csn 4550 . . . . 5 class {(0g‘(Scalar‘𝑤))}
159, 14cima 5546 . . . 4 class (𝑓 “ {(0g‘(Scalar‘𝑤))})
164, 7, 15cmpt 5133 . . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))}))
172, 3, 16cmpt 5133 . 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
181, 17wceq 1538 1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
Colors of variables: wff setvar class
This definition is referenced by:  lkrfval  36295
  Copyright terms: Public domain W3C validator