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

Theorem prdsvscaval 14857
 Description: Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.)
Hypotheses
Ref Expression
prdsbasmpt.y s
prdsbasmpt.b
prdsvscaval.t
prdsvscaval.k
prdsvscaval.s
prdsvscaval.i
prdsvscaval.r
prdsvscaval.f
prdsvscaval.g
Assertion
Ref Expression
prdsvscaval
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem prdsvscaval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prdsbasmpt.y . . 3 s
2 prdsvscaval.s . . 3
3 prdsvscaval.r . . . 4
4 prdsvscaval.i . . . 4
5 fnex 6124 . . . 4
63, 4, 5syl2anc 661 . . 3
7 prdsbasmpt.b . . 3
8 fndm 5670 . . . 4
93, 8syl 16 . . 3
10 prdsvscaval.k . . 3
11 prdsvscaval.t . . 3
121, 2, 6, 7, 9, 10, 11prdsvsca 14838 . 2
13 id 22 . . . . 5
14 fveq1 5855 . . . . 5
1513, 14oveqan12d 6300 . . . 4