This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) } )