Definition df-lfl

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)

	Ref	Expression
Assertion	df-lfl	⊢ LFnl = ( 𝑤 ∈ V ↦ { 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) ∣ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) } )

Detailed syntax breakdown

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