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