Theorem prdsplusgfval

Description: Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-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 )
	prdsplusgval.p	|- .+ = ( +g ` Y )
	prdsplusgfval.j	|- ( ph -> J e. I )
Assertion	prdsplusgfval	|- ( ph -> ( ( F .+ G ) ` J ) = ( ( F ` J ) ( +g ` ( 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		prdsplusgval.p	|- .+ = ( +g ` Y )
9		prdsplusgfval.j	|- ( ph -> J e. I )
10	1 2 3 4 5 6 7 8	prdsplusgval	|- ( ph -> ( F .+ G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )
11	10	fveq1d	|- ( ph -> ( ( F .+ G ) ` J ) = ( ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) ` J ) )
12		2fveq3	|- ( x = J -> ( +g ` ( R ` x ) ) = ( +g ` ( 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 ) ( +g ` ( R ` x ) ) ( G ` x ) ) = ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) )
16		eqid	|- ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) )
17		ovex	|- ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) e. _V
18	15 16 17	fvmpt	|- ( J e. I -> ( ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) ` J ) = ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) )
19	9 18	syl	|- ( ph -> ( ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) ` J ) = ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) )
20	11 19	eqtrd	|- ( ph -> ( ( F .+ G ) ` J ) = ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) )