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 Xs_ R )
prdsbasmpt.b
|- B = ( Base ` Y )
prdsbasmpt.s
|- ( ph -> S e. V )
prdsbasmpt.i
|- ( ph -> I e. W )
prdsbasmpt.r
|- ( ph -> R Fn I )
prdsplusgval.f
|- ( ph -> F e. B )
prdsplusgval.g
|- ( ph -> G e. B )
prdsmulrval.t
|- .x. = ( .r ` Y )
prdsmulrfval.j
|- ( ph -> J e. I )
Assertion prdsmulrfval
|- ( ph -> ( ( F .x. G ) ` J ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y
 |-  Y = ( S Xs_ R )
2 prdsbasmpt.b
 |-  B = ( Base ` Y )
3 prdsbasmpt.s
 |-  ( ph -> S e. V )
4 prdsbasmpt.i
 |-  ( ph -> I e. W )
5 prdsbasmpt.r
 |-  ( ph -> R Fn I )
6 prdsplusgval.f
 |-  ( ph -> F e. B )
7 prdsplusgval.g
 |-  ( ph -> G e. B )
8 prdsmulrval.t
 |-  .x. = ( .r ` Y )
9 prdsmulrfval.j
 |-  ( ph -> J e. I )
10 1 2 3 4 5 6 7 8 prdsmulrval
 |-  ( ph -> ( F .x. G ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) )
11 10 fveq1d
 |-  ( ph -> ( ( F .x. G ) ` J ) = ( ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) ` J ) )
12 2fveq3
 |-  ( x = J -> ( .r ` ( R ` x ) ) = ( .r ` ( 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 ` ( R ` x ) ) ( G ` x ) ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )
16 eqid
 |-  ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) )
17 ovex
 |-  ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) e. _V
18 15 16 17 fvmpt
 |-  ( J e. I -> ( ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) ` J ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )
19 9 18 syl
 |-  ( ph -> ( ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) ` J ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )
20 11 19 eqtrd
 |-  ( ph -> ( ( F .x. G ) ` J ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )