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

Theorem prdsmulrval 13697
 Description: Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.)
Hypotheses
Ref Expression
prdsbasmpt.y s
prdsbasmpt.b
prdsbasmpt.s
prdsbasmpt.i
prdsbasmpt.r
prdsplusgval.f
prdsplusgval.g
prdsmulrval.t
Assertion
Ref Expression
prdsmulrval
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem prdsmulrval
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 5961 . . . 4
63, 4, 5syl2anc 643 . . 3
7 prdsbasmpt.b . . 3
8 fndm 5544 . . . 4
93, 8syl 16 . . 3
10 prdsmulrval.t . . 3
111, 2, 6, 7, 9, 10prdsmulr 13682 . 2
12 fveq1 5727 . . . . 5
13 fveq1 5727 . . . . 5
1412, 13oveqan12d 6100 . . . 4