Metamath Proof Explorer


Theorem ldualfvadd

Description: Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualvadd.f F = LFnl W
ldualvadd.r R = Scalar W
ldualvadd.a + ˙ = + R
ldualvadd.d D = LDual W
ldualvadd.p ˙ = + D
ldualvadd.w φ W X
ldualfvadd.q ˙ = f + ˙ F × F
Assertion ldualfvadd φ ˙ = ˙

Proof

Step Hyp Ref Expression
1 ldualvadd.f F = LFnl W
2 ldualvadd.r R = Scalar W
3 ldualvadd.a + ˙ = + R
4 ldualvadd.d D = LDual W
5 ldualvadd.p ˙ = + D
6 ldualvadd.w φ W X
7 ldualfvadd.q ˙ = f + ˙ F × F
8 eqid Base W = Base W
9 eqid Base R = Base R
10 eqid R = R
11 eqid opp r R = opp r R
12 eqid k Base R , f F f R f Base W × k = k Base R , f F f R f Base W × k
13 8 3 7 1 4 2 9 10 11 12 6 ldualset φ D = Base ndx F + ndx ˙ Scalar ndx opp r R ndx k Base R , f F f R f Base W × k
14 13 fveq2d φ + D = + Base ndx F + ndx ˙ Scalar ndx opp r R ndx k Base R , f F f R f Base W × k
15 1 fvexi F V
16 id F V F V
17 16 16 ofmresex F V f + ˙ F × F V
18 15 17 ax-mp f + ˙ F × F V
19 7 18 eqeltri ˙ V
20 eqid Base ndx F + ndx ˙ Scalar ndx opp r R ndx k Base R , f F f R f Base W × k = Base ndx F + ndx ˙ Scalar ndx opp r R ndx k Base R , f F f R f Base W × k
21 20 lmodplusg ˙ V ˙ = + Base ndx F + ndx ˙ Scalar ndx opp r R ndx k Base R , f F f R f Base W × k
22 19 21 ax-mp ˙ = + Base ndx F + ndx ˙ Scalar ndx opp r R ndx k Base R , f F f R f Base W × k
23 14 5 22 3eqtr4g φ ˙ = ˙