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 V = Base W
lflset.a + ˙ = + W
lflset.d D = Scalar W
lflset.s · ˙ = W
lflset.k K = Base D
lflset.p ˙ = + D
lflset.t × ˙ = D
lflset.f F = LFnl W
Assertion lflset W X F = f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y

Proof

Step Hyp Ref Expression
1 lflset.v V = Base W
2 lflset.a + ˙ = + W
3 lflset.d D = Scalar W
4 lflset.s · ˙ = W
5 lflset.k K = Base D
6 lflset.p ˙ = + D
7 lflset.t × ˙ = D
8 lflset.f F = LFnl W
9 elex W X W V
10 fveq2 w = W Scalar w = Scalar W
11 10 3 eqtr4di w = W Scalar w = D
12 11 fveq2d w = W Base Scalar w = Base D
13 12 5 eqtr4di w = W Base Scalar w = K
14 fveq2 w = W Base w = Base W
15 14 1 eqtr4di w = W Base w = V
16 13 15 oveq12d w = W Base Scalar w Base w = K V
17 fveq2 w = W + w = + W
18 17 2 eqtr4di w = W + w = + ˙
19 fveq2 w = W w = W
20 19 4 eqtr4di w = W w = · ˙
21 20 oveqd w = W r w x = r · ˙ x
22 eqidd w = W y = y
23 18 21 22 oveq123d w = W r w x + w y = r · ˙ x + ˙ y
24 23 fveq2d w = W f r w x + w y = f r · ˙ x + ˙ y
25 11 fveq2d w = W + Scalar w = + D
26 25 6 eqtr4di w = W + Scalar w = ˙
27 11 fveq2d w = W Scalar w = D
28 27 7 eqtr4di w = W Scalar w = × ˙
29 28 oveqd w = W r Scalar w f x = r × ˙ f x
30 eqidd w = W f y = f y
31 26 29 30 oveq123d w = W r Scalar w f x + Scalar w f y = r × ˙ f x ˙ f y
32 24 31 eqeq12d w = W f r w x + w y = r Scalar w f x + Scalar w f y f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
33 15 32 raleqbidv w = W y Base w f r w x + w y = r Scalar w f x + Scalar w f y y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
34 15 33 raleqbidv w = W x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
35 13 34 raleqbidv w = W r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
36 16 35 rabeqbidv w = W f Base Scalar w Base w | r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y = f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
37 df-lfl LFnl = w V f Base Scalar w Base w | r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y
38 ovex K V V
39 38 rabex f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y V
40 36 37 39 fvmpt W V LFnl W = f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
41 8 40 syl5eq W V F = f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
42 9 41 syl W X F = f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y