Theorem prdsmulrval

Description: Value of a componentwise ring product in a structure product. (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 )
Assertion	prdsmulrval	|- ( ph -> ( F .x. G ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( 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		prdsmulrval.t	|- .x. = ( .r ` 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	prdsmulr	|- ( ph -> .x. = ( y e. B , z e. B |-> ( x e. I |-> ( ( y ` x ) ( .r ` ( 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 ) ( .r ` ( R ` x ) ) ( z ` x ) ) = ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) )
16	15	adantl	|- ( ( ph /\ ( y = F /\ z = G ) ) -> ( ( y ` x ) ( .r ` ( R ` x ) ) ( z ` x ) ) = ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) )
17	16	mpteq2dv	|- ( ( ph /\ ( y = F /\ z = G ) ) -> ( x e. I |-> ( ( y ` x ) ( .r ` ( R ` x ) ) ( z ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) )
18	4	mptexd	|- ( ph -> ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) e. _V )
19	12 17 6 7 18	ovmpod	|- ( ph -> ( F .x. G ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) )