Metamath Proof Explorer


Theorem prdsplusgval

Description: Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015) (Revised by Mario Carneiro, 15-Aug-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 )
prdsplusgval.p
|- .+ = ( +g ` Y )
Assertion prdsplusgval
|- ( ph -> ( F .+ G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )

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 prdsplusgval.p
 |-  .+ = ( +g ` Y )
9 fnex
 |-  ( ( R Fn I /\ I e. W ) -> R e. _V )
10 5 4 9 syl2anc
 |-  ( ph -> R e. _V )
11 5 fndmd
 |-  ( ph -> dom R = I )
12 1 3 10 2 11 8 prdsplusg
 |-  ( ph -> .+ = ( y e. B , z e. B |-> ( x e. I |-> ( ( y ` x ) ( +g ` ( R ` x ) ) ( z ` x ) ) ) ) )
13 fveq1
 |-  ( y = F -> ( y ` x ) = ( F ` x ) )
14 fveq1
 |-  ( z = G -> ( z ` x ) = ( G ` x ) )
15 13 14 oveqan12d
 |-  ( ( y = F /\ z = G ) -> ( ( y ` x ) ( +g ` ( R ` x ) ) ( z ` x ) ) = ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) )
16 15 adantl
 |-  ( ( ph /\ ( y = F /\ z = G ) ) -> ( ( y ` x ) ( +g ` ( R ` x ) ) ( z ` x ) ) = ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) )
17 16 mpteq2dv
 |-  ( ( ph /\ ( y = F /\ z = G ) ) -> ( x e. I |-> ( ( y ` x ) ( +g ` ( R ` x ) ) ( z ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )
18 4 mptexd
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) e. _V )
19 12 17 6 7 18 ovmpod
 |-  ( ph -> ( F .+ G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )