Metamath Proof Explorer


Theorem dvafvadd

Description: The vector sum operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvafvadd.h H = LHyp K
dvafvadd.t T = LTrn K W
dvafvadd.u U = DVecA K W
dvafvadd.v + ˙ = + U
Assertion dvafvadd K X W H + ˙ = f T , g T f g

Proof

Step Hyp Ref Expression
1 dvafvadd.h H = LHyp K
2 dvafvadd.t T = LTrn K W
3 dvafvadd.u U = DVecA K W
4 dvafvadd.v + ˙ = + U
5 eqid TEndo K W = TEndo K W
6 eqid EDRing K W = EDRing K W
7 1 2 5 6 3 dvaset K X W H U = Base ndx T + ndx f T , g T f g Scalar ndx EDRing K W ndx s TEndo K W , f T s f
8 7 fveq2d K X W H + U = + Base ndx T + ndx f T , g T f g Scalar ndx EDRing K W ndx s TEndo K W , f T s f
9 2 fvexi T V
10 9 9 mpoex f T , g T f g V
11 eqid Base ndx T + ndx f T , g T f g Scalar ndx EDRing K W ndx s TEndo K W , f T s f = Base ndx T + ndx f T , g T f g Scalar ndx EDRing K W ndx s TEndo K W , f T s f
12 11 lmodplusg f T , g T f g V f T , g T f g = + Base ndx T + ndx f T , g T f g Scalar ndx EDRing K W ndx s TEndo K W , f T s f
13 10 12 ax-mp f T , g T f g = + Base ndx T + ndx f T , g T f g Scalar ndx EDRing K W ndx s TEndo K W , f T s f
14 8 4 13 3eqtr4g K X W H + ˙ = f T , g T f g