Metamath Proof Explorer

Theorem lflset

Description: The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lflset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lflset.a ⊢ + = ( +g ‘ 𝑊 )
lflset.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lflset.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lflset.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lflset.p ⊢ ⨣ = ( +g ‘ 𝐷 )
lflset.t ⊢ × = ( .r ‘ 𝐷 )
lflset.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lflset ( 𝑊 ∈ 𝑋 → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 lflset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lflset.a ⊢ + = ( +g ‘ 𝑊 )
3 lflset.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
4 lflset.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 lflset.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
6 lflset.p ⊢ ⨣ = ( +g ‘ 𝐷 )
7 lflset.t ⊢ × = ( .r ‘ 𝐷 )
8 lflset.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
9 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
10 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
11 10 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐷 )
12 11 fveq2d ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝐷 ) )
13 12 5 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝐾 )
14 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
15 14 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
16 13 15 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) = ( 𝐾 ↑m 𝑉 ) )
17 fveq2 ⊢ ( 𝑤 = 𝑊 → ( +g ‘ 𝑤 ) = ( +g ‘ 𝑊 ) )
18 17 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( +g ‘ 𝑤 ) = + )
19 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
20 19 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
21 20 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) = ( 𝑟 · 𝑥 ) )
22 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑦 = 𝑦 )
23 18 21 22 oveq123d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) = ( ( 𝑟 · 𝑥 ) + 𝑦 ) )
24 23 fveq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) )
25 11 fveq2d ⊢ ( 𝑤 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑤 ) ) = ( +g ‘ 𝐷 ) )
26 25 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑤 ) ) = ⨣ )
27 11 fveq2d ⊢ ( 𝑤 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑤 ) ) = ( .r ‘ 𝐷 ) )
28 27 7 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑤 ) ) = × )
29 28 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) = ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) )
30 eqidd ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
31 26 29 30 oveq123d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) )
32 24 31 eqeq12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
33 15 32 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
34 15 33 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
35 13 34 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
36 16 35 rabeqbidv ⊢ ( 𝑤 = 𝑊 → { 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) ∣ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )
37 df-lfl ⊢ LFnl = ( 𝑤 ∈ V ↦ { 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) ∣ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) } )
38 ovex ⊢ ( 𝐾 ↑m 𝑉 ) ∈ V
39 38 rabex ⊢ { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } ∈ V
40 36 37 39 fvmpt ⊢ ( 𝑊 ∈ V → ( LFnl ‘ 𝑊 ) = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )
41 8 40 syl5eq ⊢ ( 𝑊 ∈ V → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )
42 9 41 syl ⊢ ( 𝑊 ∈ 𝑋 → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )