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 37079
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 37078 . 2 class LKer
2 vw . . 3 setvar 𝑤
3 cvv 3430 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1540 . . . . 5 class 𝑤
6 clfn 37050 . . . . 5 class LFnl
75, 6cfv 6430 . . . 4 class (LFnl‘𝑤)
84cv 1540 . . . . . 6 class 𝑓
98ccnv 5587 . . . . 5 class 𝑓
10 csca 16946 . . . . . . . 8 class Scalar
115, 10cfv 6430 . . . . . . 7 class (Scalar‘𝑤)
12 c0g 17131 . . . . . . 7 class 0g
1311, 12cfv 6430 . . . . . 6 class (0g‘(Scalar‘𝑤))
1413csn 4566 . . . . 5 class {(0g‘(Scalar‘𝑤))}
159, 14cima 5591 . . . 4 class (𝑓 “ {(0g‘(Scalar‘𝑤))})
164, 7, 15cmpt 5161 . . 3 class (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))}))
172, 3, 16cmpt 5161 . 2 class (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
181, 17wceq 1541 1 wff LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 “ {(0g‘(Scalar‘𝑤))})))
Colors of variables: wff setvar class
This definition is referenced by:  lkrfval  37080
  Copyright terms: Public domain W3C validator