Metamath Proof Explorer


Theorem pwsplusgval

Description: Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsplusgval.y Y=R𝑠I
pwsplusgval.b B=BaseY
pwsplusgval.r φRV
pwsplusgval.i φIW
pwsplusgval.f φFB
pwsplusgval.g φGB
pwsplusgval.a +˙=+R
pwsplusgval.p ˙=+Y
Assertion pwsplusgval φF˙G=F+˙fG

Proof

Step Hyp Ref Expression
1 pwsplusgval.y Y=R𝑠I
2 pwsplusgval.b B=BaseY
3 pwsplusgval.r φRV
4 pwsplusgval.i φIW
5 pwsplusgval.f φFB
6 pwsplusgval.g φGB
7 pwsplusgval.a +˙=+R
8 pwsplusgval.p ˙=+Y
9 eqid ScalarR𝑠I×R=ScalarR𝑠I×R
10 eqid BaseScalarR𝑠I×R=BaseScalarR𝑠I×R
11 fvexd φScalarRV
12 fnconstg RVI×RFnI
13 3 12 syl φI×RFnI
14 eqid ScalarR=ScalarR
15 1 14 pwsval RVIWY=ScalarR𝑠I×R
16 3 4 15 syl2anc φY=ScalarR𝑠I×R
17 16 fveq2d φBaseY=BaseScalarR𝑠I×R
18 2 17 eqtrid φB=BaseScalarR𝑠I×R
19 5 18 eleqtrd φFBaseScalarR𝑠I×R
20 6 18 eleqtrd φGBaseScalarR𝑠I×R
21 eqid +ScalarR𝑠I×R=+ScalarR𝑠I×R
22 9 10 11 4 13 19 20 21 prdsplusgval φF+ScalarR𝑠I×RG=xIFx+I×RxGx
23 fvconst2g RVxII×Rx=R
24 3 23 sylan φxII×Rx=R
25 24 fveq2d φxI+I×Rx=+R
26 25 7 eqtr4di φxI+I×Rx=+˙
27 26 oveqd φxIFx+I×RxGx=Fx+˙Gx
28 27 mpteq2dva φxIFx+I×RxGx=xIFx+˙Gx
29 22 28 eqtrd φF+ScalarR𝑠I×RG=xIFx+˙Gx
30 16 fveq2d φ+Y=+ScalarR𝑠I×R
31 8 30 eqtrid φ˙=+ScalarR𝑠I×R
32 31 oveqd φF˙G=F+ScalarR𝑠I×RG
33 fvexd φxIFxV
34 fvexd φxIGxV
35 eqid BaseR=BaseR
36 1 35 2 3 4 5 pwselbas φF:IBaseR
37 36 feqmptd φF=xIFx
38 1 35 2 3 4 6 pwselbas φG:IBaseR
39 38 feqmptd φG=xIGx
40 4 33 34 37 39 offval2 φF+˙fG=xIFx+˙Gx
41 29 32 40 3eqtr4d φF˙G=F+˙fG