Definition df-lfl 36999

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

Step	Hyp	Ref	Expression
1		clfn 36998	. 2 class LFnl
2		vw	. . 3 setvar 𝑤
3		cvv 3422	. . 3 class V
4		vr	. . . . . . . . . . . 12 setvar 𝑟
5	4	cv 1538	. . . . . . . . . . 11 class 𝑟
6		vx	. . . . . . . . . . . 12 setvar 𝑥
7	6	cv 1538	. . . . . . . . . . 11 class 𝑥
8	2	cv 1538	. . . . . . . . . . . 12 class 𝑤
9		cvsca 16892	. . . . . . . . . . . 12 class ·𝑠
10	8, 9	cfv 6418	. . . . . . . . . . 11 class ( ·𝑠 ‘𝑤)
11	5, 7, 10	co 7255	. . . . . . . . . 10 class (𝑟( ·𝑠 ‘𝑤)𝑥)
12		vy	. . . . . . . . . . 11 setvar 𝑦
13	12	cv 1538	. . . . . . . . . 10 class 𝑦
14		cplusg 16888	. . . . . . . . . . 11 class +g
15	8, 14	cfv 6418	. . . . . . . . . 10 class (+g‘𝑤)
16	11, 13, 15	co 7255	. . . . . . . . 9 class ((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)
17		vf	. . . . . . . . . 10 setvar 𝑓
18	17	cv 1538	. . . . . . . . 9 class 𝑓
19	16, 18	cfv 6418	. . . . . . . 8 class (𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦))
20	7, 18	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑥)
21		csca 16891	. . . . . . . . . . . 12 class Scalar
22	8, 21	cfv 6418	. . . . . . . . . . 11 class (Scalar‘𝑤)
23		cmulr 16889	. . . . . . . . . . 11 class .r
24	22, 23	cfv 6418	. . . . . . . . . 10 class (.r‘(Scalar‘𝑤))
25	5, 20, 24	co 7255	. . . . . . . . 9 class (𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))
26	13, 18	cfv 6418	. . . . . . . . 9 class (𝑓‘𝑦)
27	22, 14	cfv 6418	. . . . . . . . 9 class (+g‘(Scalar‘𝑤))
28	25, 26, 27	co 7255	. . . . . . . 8 class ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))
29	19, 28	wceq 1539	. . . . . . 7 wff (𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))
30		cbs 16840	. . . . . . . 8 class Base
31	8, 30	cfv 6418	. . . . . . 7 class (Base‘𝑤)
32	29, 12, 31	wral 3063	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))
33	32, 6, 31	wral 3063	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))
34	22, 30	cfv 6418	. . . . 5 class (Base‘(Scalar‘𝑤))
35	33, 4, 34	wral 3063	. . . 4 wff ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))
36		cmap 8573	. . . . 5 class ↑m
37	34, 31, 36	co 7255	. . . 4 class ((Base‘(Scalar‘𝑤)) ↑m (Base‘𝑤))
38	35, 17, 37	crab 3067	. . 3 class {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑m (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))}
39	2, 3, 38	cmpt 5153	. 2 class (𝑤 ∈ V ↦ {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑m (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))})
40	1, 39	wceq 1539	1 wff LFnl = (𝑤 ∈ V ↦ {𝑓 ∈ ((Base‘(Scalar‘𝑤)) ↑m (Base‘𝑤)) ∣ ∀𝑟 ∈ (Base‘(Scalar‘𝑤))∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)(𝑓‘((𝑟( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)𝑦)) = ((𝑟(.r‘(Scalar‘𝑤))(𝑓‘𝑥))(+g‘(Scalar‘𝑤))(𝑓‘𝑦))})

This definition is referenced by:  lflset  37000