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 33825
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‘𝑤)) ↑𝑚 (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))})
Distinct variable group:   𝑥,𝑤,𝑦,𝑟,𝑓

Detailed syntax breakdown of Definition df-lfl
StepHypRef Expression
1 clfn 33824 . 2 class LFnl
2 vw . . 3 setvar 𝑤
3 cvv 3186 . . 3 class V
4 vr . . . . . . . . . . . 12 setvar 𝑟
54cv 1479 . . . . . . . . . . 11 class 𝑟
6 vx . . . . . . . . . . . 12 setvar 𝑥
76cv 1479 . . . . . . . . . . 11 class 𝑥
82cv 1479 . . . . . . . . . . . 12 class 𝑤
9 cvsca 15866 . . . . . . . . . . . 12 class ·𝑠
108, 9cfv 5847 . . . . . . . . . . 11 class ( ·𝑠𝑤)
115, 7, 10co 6604 . . . . . . . . . 10 class (𝑟( ·𝑠𝑤)𝑥)
12 vy . . . . . . . . . . 11 setvar 𝑦
1312cv 1479 . . . . . . . . . 10 class 𝑦
14 cplusg 15862 . . . . . . . . . . 11 class +g
158, 14cfv 5847 . . . . . . . . . 10 class (+g𝑤)
1611, 13, 15co 6604 . . . . . . . . 9 class ((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)
17 vf . . . . . . . . . 10 setvar 𝑓
1817cv 1479 . . . . . . . . 9 class 𝑓
1916, 18cfv 5847 . . . . . . . 8 class (𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦))
207, 18cfv 5847 . . . . . . . . . 10 class (𝑓𝑥)
21 csca 15865 . . . . . . . . . . . 12 class Scalar
228, 21cfv 5847 . . . . . . . . . . 11 class (Scalar‘𝑤)
23 cmulr 15863 . . . . . . . . . . 11 class .r
2422, 23cfv 5847 . . . . . . . . . 10 class (.r‘(Scalar‘𝑤))
255, 20, 24co 6604 . . . . . . . . 9 class (𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))
2613, 18cfv 5847 . . . . . . . . 9 class (𝑓𝑦)
2722, 14cfv 5847 . . . . . . . . 9 class (+g‘(Scalar‘𝑤))
2825, 26, 27co 6604 . . . . . . . 8 class ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))
2919, 28wceq 1480 . . . . . . 7 wff (𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))
30 cbs 15781 . . . . . . . 8 class Base
318, 30cfv 5847 . . . . . . 7 class (Base‘𝑤)
3229, 12, 31wral 2907 . . . . . 6 wff 𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))
3332, 6, 31wral 2907 . . . . 5 wff 𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))
3422, 30cfv 5847 . . . . 5 class (Base‘(Scalar‘𝑤))
3533, 4, 34wral 2907 . . . 4 wff 𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))
36 cmap 7802 . . . . 5 class 𝑚
3734, 31, 36co 6604 . . . 4 class ((Base‘(Scalar‘𝑤)) ↑𝑚 (Base‘𝑤))
3835, 17, 37crab 2911 . . 3 class {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑𝑚 (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))}
392, 3, 38cmpt 4673 . 2 class (𝑤 ∈ V ↦ {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑𝑚 (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))})
401, 39wceq 1480 1 wff LFnl = (𝑤 ∈ V ↦ {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑𝑚 (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠𝑤)𝑥)(+g𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓𝑥))(+g‘(Scalar‘𝑤))(𝑓𝑦))})
Colors of variables: wff setvar class
This definition is referenced by:  lflset  33826
  Copyright terms: Public domain W3C validator