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{⨉}_{𝑠}R$$
	prdsbasmpt.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsbasmpt.s	$$⊢\phi \to S\in V$$
	prdsbasmpt.i	$$⊢\phi \to I\in W$$
	prdsbasmpt.r	$$⊢\phi \to RFnI$$
	prdsplusgval.f	$$⊢\phi \to F\in B$$
	prdsplusgval.g	$$⊢\phi \to G\in B$$
	prdsmulrval.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	prdsmulrfval.j	$$⊢\phi \to J\in I$$
Assertion	prdsmulrfval	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\left(J\right)=F\left(J\right){\cdot }_{R\left(J\right)}G\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsbasmpt.b	$$⊢B={\mathrm{Base}}_Y$$
3		prdsbasmpt.s	$$⊢\phi \to S\in V$$
4		prdsbasmpt.i	$$⊢\phi \to I\in W$$
5		prdsbasmpt.r	$$⊢\phi \to RFnI$$
6		prdsplusgval.f	$$⊢\phi \to F\in B$$
7		prdsplusgval.g	$$⊢\phi \to G\in B$$
8		prdsmulrval.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
9		prdsmulrfval.j	$$⊢\phi \to J\in I$$
10	1 2 3 4 5 6 7 8	prdsmulrval	$$⊢\phi \to F\underset{\dot{}}{·}G=\left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)$$
11	10	fveq1d	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\left(J\right)=\left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)\left(J\right)$$
12		2fveq3	$$⊢x=J\to {\cdot }_{R\left(x\right)}={\cdot }_{R\left(J\right)}$$
13		fveq2	$$⊢x=J\to F\left(x\right)=F\left(J\right)$$
14		fveq2	$$⊢x=J\to G\left(x\right)=G\left(J\right)$$
15	12 13 14	oveq123d	$$⊢x=J\to F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)=F\left(J\right){\cdot }_{R\left(J\right)}G\left(J\right)$$
16		eqid	$$⊢\left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)=\left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)$$
17		ovex	$$⊢F\left(J\right){\cdot }_{R\left(J\right)}G\left(J\right)\in \mathrm{V}$$
18	15 16 17	fvmpt	$$⊢J\in I\to \left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)\left(J\right)=F\left(J\right){\cdot }_{R\left(J\right)}G\left(J\right)$$
19	9 18	syl	$$⊢\phi \to \left(x\in I⟼F\left(x\right){\cdot }_{R\left(x\right)}G\left(x\right)\right)\left(J\right)=F\left(J\right){\cdot }_{R\left(J\right)}G\left(J\right)$$
20	11 19	eqtrd	$$⊢\phi \to \left(F\underset{\dot{}}{·}G\right)\left(J\right)=F\left(J\right){\cdot }_{R\left(J\right)}G\left(J\right)$$