Metamath Proof Explorer


Theorem ldualset

Description: Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in Holland95 p. 218. This allows us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppR ring, for convenience. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualset.v V = Base W
ldualset.a + ˙ = + R
ldualset.p ˙ = f + ˙ F × F
ldualset.f F = LFnl W
ldualset.d D = LDual W
ldualset.r R = Scalar W
ldualset.k K = Base R
ldualset.t · ˙ = R
ldualset.o O = opp r R
ldualset.s ˙ = k K , f F f · ˙ f V × k
ldualset.w φ W X
Assertion ldualset φ D = Base ndx F + ndx ˙ Scalar ndx O ndx ˙

Proof

Step Hyp Ref Expression
1 ldualset.v V = Base W
2 ldualset.a + ˙ = + R
3 ldualset.p ˙ = f + ˙ F × F
4 ldualset.f F = LFnl W
5 ldualset.d D = LDual W
6 ldualset.r R = Scalar W
7 ldualset.k K = Base R
8 ldualset.t · ˙ = R
9 ldualset.o O = opp r R
10 ldualset.s ˙ = k K , f F f · ˙ f V × k
11 ldualset.w φ W X
12 elex W X W V
13 fveq2 w = W LFnl w = LFnl W
14 13 4 eqtr4di w = W LFnl w = F
15 14 opeq2d w = W Base ndx LFnl w = Base ndx F
16 fveq2 w = W Scalar w = Scalar W
17 16 6 eqtr4di w = W Scalar w = R
18 17 fveq2d w = W + Scalar w = + R
19 18 2 eqtr4di w = W + Scalar w = + ˙
20 ofeq + Scalar w = + ˙ f + Scalar w = f + ˙
21 19 20 syl w = W f + Scalar w = f + ˙
22 14 sqxpeqd w = W LFnl w × LFnl w = F × F
23 21 22 reseq12d w = W f + Scalar w LFnl w × LFnl w = f + ˙ F × F
24 23 3 eqtr4di w = W f + Scalar w LFnl w × LFnl w = ˙
25 24 opeq2d w = W + ndx f + Scalar w LFnl w × LFnl w = + ndx ˙
26 17 fveq2d w = W opp r Scalar w = opp r R
27 26 9 eqtr4di w = W opp r Scalar w = O
28 27 opeq2d w = W Scalar ndx opp r Scalar w = Scalar ndx O
29 15 25 28 tpeq123d w = W Base ndx LFnl w + ndx f + Scalar w LFnl w × LFnl w Scalar ndx opp r Scalar w = Base ndx F + ndx ˙ Scalar ndx O
30 17 fveq2d w = W Base Scalar w = Base R
31 30 7 eqtr4di w = W Base Scalar w = K
32 17 fveq2d w = W Scalar w = R
33 32 8 eqtr4di w = W Scalar w = · ˙
34 ofeq Scalar w = · ˙ f Scalar w = f · ˙
35 33 34 syl w = W f Scalar w = f · ˙
36 eqidd w = W f = f
37 fveq2 w = W Base w = Base W
38 37 1 eqtr4di w = W Base w = V
39 38 xpeq1d w = W Base w × k = V × k
40 35 36 39 oveq123d w = W f Scalar w f Base w × k = f · ˙ f V × k
41 31 14 40 mpoeq123dv w = W k Base Scalar w , f LFnl w f Scalar w f Base w × k = k K , f F f · ˙ f V × k
42 41 10 eqtr4di w = W k Base Scalar w , f LFnl w f Scalar w f Base w × k = ˙
43 42 opeq2d w = W ndx k Base Scalar w , f LFnl w f Scalar w f Base w × k = ndx ˙
44 43 sneqd w = W ndx k Base Scalar w , f LFnl w f Scalar w f Base w × k = ndx ˙
45 29 44 uneq12d w = W Base ndx LFnl w + ndx f + Scalar w LFnl w × LFnl w Scalar ndx opp r Scalar w ndx k Base Scalar w , f LFnl w f Scalar w f Base w × k = Base ndx F + ndx ˙ Scalar ndx O ndx ˙
46 df-ldual LDual = w V Base ndx LFnl w + ndx f + Scalar w LFnl w × LFnl w Scalar ndx opp r Scalar w ndx k Base Scalar w , f LFnl w f Scalar w f Base w × k
47 tpex Base ndx F + ndx ˙ Scalar ndx O V
48 snex ndx ˙ V
49 47 48 unex Base ndx F + ndx ˙ Scalar ndx O ndx ˙ V
50 45 46 49 fvmpt W V LDual W = Base ndx F + ndx ˙ Scalar ndx O ndx ˙
51 5 50 syl5eq W V D = Base ndx F + ndx ˙ Scalar ndx O ndx ˙
52 11 12 51 3syl φ D = Base ndx F + ndx ˙ Scalar ndx O ndx ˙