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

Definition df-lfl 37928
Description: Define the set of all linear functionals (maps from vectors to the ring) of a left module or left vector space. (Contributed by NM, 15-Apr-2014.)
Assertion
Ref Expression
df-lfl LFnl = (𝑀 ∈ V ↦ {𝑓 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m (Baseβ€˜π‘€)) ∣ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘€))βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))})
Distinct variable group:   π‘₯,𝑀,𝑦,π‘Ÿ,𝑓

Detailed syntax breakdown of Definition df-lfl
StepHypRef Expression
1 clfn 37927 . 2 class LFnl
2 vw . . 3 setvar 𝑀
3 cvv 3475 . . 3 class V
4 vr . . . . . . . . . . . 12 setvar π‘Ÿ
54cv 1541 . . . . . . . . . . 11 class π‘Ÿ
6 vx . . . . . . . . . . . 12 setvar π‘₯
76cv 1541 . . . . . . . . . . 11 class π‘₯
82cv 1541 . . . . . . . . . . . 12 class 𝑀
9 cvsca 17201 . . . . . . . . . . . 12 class ·𝑠
108, 9cfv 6544 . . . . . . . . . . 11 class ( ·𝑠 β€˜π‘€)
115, 7, 10co 7409 . . . . . . . . . 10 class (π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)
12 vy . . . . . . . . . . 11 setvar 𝑦
1312cv 1541 . . . . . . . . . 10 class 𝑦
14 cplusg 17197 . . . . . . . . . . 11 class +g
158, 14cfv 6544 . . . . . . . . . 10 class (+gβ€˜π‘€)
1611, 13, 15co 7409 . . . . . . . . 9 class ((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)
17 vf . . . . . . . . . 10 setvar 𝑓
1817cv 1541 . . . . . . . . 9 class 𝑓
1916, 18cfv 6544 . . . . . . . 8 class (π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦))
207, 18cfv 6544 . . . . . . . . . 10 class (π‘“β€˜π‘₯)
21 csca 17200 . . . . . . . . . . . 12 class Scalar
228, 21cfv 6544 . . . . . . . . . . 11 class (Scalarβ€˜π‘€)
23 cmulr 17198 . . . . . . . . . . 11 class .r
2422, 23cfv 6544 . . . . . . . . . 10 class (.rβ€˜(Scalarβ€˜π‘€))
255, 20, 24co 7409 . . . . . . . . 9 class (π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))
2613, 18cfv 6544 . . . . . . . . 9 class (π‘“β€˜π‘¦)
2722, 14cfv 6544 . . . . . . . . 9 class (+gβ€˜(Scalarβ€˜π‘€))
2825, 26, 27co 7409 . . . . . . . 8 class ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))
2919, 28wceq 1542 . . . . . . 7 wff (π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))
30 cbs 17144 . . . . . . . 8 class Base
318, 30cfv 6544 . . . . . . 7 class (Baseβ€˜π‘€)
3229, 12, 31wral 3062 . . . . . 6 wff βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))
3332, 6, 31wral 3062 . . . . 5 wff βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))
3422, 30cfv 6544 . . . . 5 class (Baseβ€˜(Scalarβ€˜π‘€))
3533, 4, 34wral 3062 . . . 4 wff βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘€))βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))
36 cmap 8820 . . . . 5 class ↑m
3734, 31, 36co 7409 . . . 4 class ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m (Baseβ€˜π‘€))
3835, 17, 37crab 3433 . . 3 class {𝑓 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m (Baseβ€˜π‘€)) ∣ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘€))βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))}
392, 3, 38cmpt 5232 . 2 class (𝑀 ∈ V ↦ {𝑓 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m (Baseβ€˜π‘€)) ∣ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘€))βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))})
401, 39wceq 1542 1 wff LFnl = (𝑀 ∈ V ↦ {𝑓 ∈ ((Baseβ€˜(Scalarβ€˜π‘€)) ↑m (Baseβ€˜π‘€)) ∣ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘€))βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)(π‘“β€˜((π‘Ÿ( ·𝑠 β€˜π‘€)π‘₯)(+gβ€˜π‘€)𝑦)) = ((π‘Ÿ(.rβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘₯))(+gβ€˜(Scalarβ€˜π‘€))(π‘“β€˜π‘¦))})
Colors of variables: wff setvar class
This definition is referenced by:  lflset  37929
  Copyright terms: Public domain W3C validator