Metamath Proof Explorer


Theorem prdsmulrfval

Description: Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses prdsbasmpt.y Y = S 𝑠 R
prdsbasmpt.b B = Base Y
prdsbasmpt.s φ S V
prdsbasmpt.i φ I W
prdsbasmpt.r φ R Fn I
prdsplusgval.f φ F B
prdsplusgval.g φ G B
prdsmulrval.t · ˙ = Y
prdsmulrfval.j φ J I
Assertion prdsmulrfval φ F · ˙ G J = F J R J G J

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y Y = S 𝑠 R
2 prdsbasmpt.b B = Base Y
3 prdsbasmpt.s φ S V
4 prdsbasmpt.i φ I W
5 prdsbasmpt.r φ R Fn I
6 prdsplusgval.f φ F B
7 prdsplusgval.g φ G B
8 prdsmulrval.t · ˙ = Y
9 prdsmulrfval.j φ J I
10 1 2 3 4 5 6 7 8 prdsmulrval φ F · ˙ G = x I F x R x G x
11 10 fveq1d φ F · ˙ G J = x I F x R x G x J
12 2fveq3 x = J R x = R J
13 fveq2 x = J F x = F J
14 fveq2 x = J G x = G J
15 12 13 14 oveq123d x = J F x R x G x = F J R J G J
16 eqid x I F x R x G x = x I F x R x G x
17 ovex F J R J G J V
18 15 16 17 fvmpt J I x I F x R x G x J = F J R J G J
19 9 18 syl φ x I F x R x G x J = F J R J G J
20 11 19 eqtrd φ F · ˙ G J = F J R J G J