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=LHypK
dvafvadd.t T=LTrnKW
dvafvadd.u U=DVecAKW
dvafvadd.v +˙=+U
Assertion dvafvadd KXWH+˙=fT,gTfg

Proof

Step Hyp Ref Expression
1 dvafvadd.h H=LHypK
2 dvafvadd.t T=LTrnKW
3 dvafvadd.u U=DVecAKW
4 dvafvadd.v +˙=+U
5 eqid TEndoKW=TEndoKW
6 eqid EDRingKW=EDRingKW
7 1 2 5 6 3 dvaset KXWHU=BasendxT+ndxfT,gTfgScalarndxEDRingKWndxsTEndoKW,fTsf
8 7 fveq2d KXWH+U=+BasendxT+ndxfT,gTfgScalarndxEDRingKWndxsTEndoKW,fTsf
9 2 fvexi TV
10 9 9 mpoex fT,gTfgV
11 eqid BasendxT+ndxfT,gTfgScalarndxEDRingKWndxsTEndoKW,fTsf=BasendxT+ndxfT,gTfgScalarndxEDRingKWndxsTEndoKW,fTsf
12 11 lmodplusg fT,gTfgVfT,gTfg=+BasendxT+ndxfT,gTfgScalarndxEDRingKWndxsTEndoKW,fTsf
13 10 12 ax-mp fT,gTfg=+BasendxT+ndxfT,gTfgScalarndxEDRingKWndxsTEndoKW,fTsf
14 8 4 13 3eqtr4g KXWH+˙=fT,gTfg