This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )