Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prdsplusgval Structured version   Unicode version

Theorem prdsplusgval 13726
 Description: Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
Hypotheses
Ref Expression
prdsbasmpt.y s
prdsbasmpt.b
prdsbasmpt.s
prdsbasmpt.i
prdsbasmpt.r
prdsplusgval.f
prdsplusgval.g
prdsplusgval.p
Assertion
Ref Expression
prdsplusgval
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem prdsplusgval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prdsbasmpt.y . . 3 s
2 prdsbasmpt.s . . 3
3 prdsbasmpt.r . . . 4
4 prdsbasmpt.i . . . 4
5 fnex 5990 . . . 4
63, 4, 5syl2anc 644 . . 3
7 prdsbasmpt.b . . 3
8 fndm 5573 . . . 4
93, 8syl 16 . . 3
10 prdsplusgval.p . . 3
111, 2, 6, 7, 9, 10prdsplusg 13712 . 2
12 fveq1 5756 . . . . 5
13 fveq1 5756 . . . . 5
1412, 13oveqan12d 6129 . . . 4