Theorem pwsmulrval

Description: Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsplusgval.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsplusgval.b	$$⊢B={\mathrm{Base}}_Y$$
	pwsplusgval.r	$$⊢\phi \to R\in V$$
	pwsplusgval.i	$$⊢\phi \to I\in W$$
	pwsplusgval.f	$$⊢\phi \to F\in B$$
	pwsplusgval.g	$$⊢\phi \to G\in B$$
	pwsmulrval.a	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	pwsmulrval.p	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
Assertion	pwsmulrval	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=F{\underset{\dot{}}{·}}_{f}G$$

Proof

Step	Hyp	Ref	Expression
1		pwsplusgval.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsplusgval.b	$$⊢B={\mathrm{Base}}_Y$$
3		pwsplusgval.r	$$⊢\phi \to R\in V$$
4		pwsplusgval.i	$$⊢\phi \to I\in W$$
5		pwsplusgval.f	$$⊢\phi \to F\in B$$
6		pwsplusgval.g	$$⊢\phi \to G\in B$$
7		pwsmulrval.a	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		pwsmulrval.p	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
9		eqid	$$⊢\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
11		fvexd	$$⊢\phi \to \mathrm{Scalar}\left(R\right)\in \mathrm{V}$$
12		fnconstg	$$⊢R\in V\to \left(I\times \left\{R\right\}\right)FnI$$
13	3 12	syl	$$⊢\phi \to \left(I\times \left\{R\right\}\right)FnI$$
14		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
15	1 14	pwsval	$$⊢\left(R\in V\wedge I\in W\right)\to Y=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
16	3 4 15	syl2anc	$$⊢\phi \to Y=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
17	16	fveq2d	$$⊢\phi \to {\mathrm{Base}}_Y={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
18	2 17	syl5eq	$$⊢\phi \to B={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
19	5 18	eleqtrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
20	6 18	eleqtrd	$$⊢\phi \to G\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
21		eqid	$$⊢{\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}={\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
22	9 10 11 4 13 19 20 21	prdsmulrval	$$⊢\phi \to F{\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}G=\left(x\in I⟼F\left(x\right){\cdot }_{\left(I\times \left\{R\right\}\right)\left(x\right)}G\left(x\right)\right)$$
23		fvconst2g	$$⊢\left(R\in V\wedge x\in I\right)\to \left(I\times \left\{R\right\}\right)\left(x\right)=R$$
24	3 23	sylan	$$⊢\left(\phi \wedge x\in I\right)\to \left(I\times \left\{R\right\}\right)\left(x\right)=R$$
25	24	fveq2d	$$⊢\left(\phi \wedge x\in I\right)\to {\cdot }_{\left(I\times \left\{R\right\}\right)\left(x\right)}={\cdot }_R$$
26	25 7	syl6eqr	$$⊢\left(\phi \wedge x\in I\right)\to {\cdot }_{\left(I\times \left\{R\right\}\right)\left(x\right)}=\underset{\dot{}}{·}$$
27	26	oveqd	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right){\cdot }_{\left(I\times \left\{R\right\}\right)\left(x\right)}G\left(x\right)=F\left(x\right)\underset{\dot{}}{·}G\left(x\right)$$
28	27	mpteq2dva	$$⊢\phi \to \left(x\in I⟼F\left(x\right){\cdot }_{\left(I\times \left\{R\right\}\right)\left(x\right)}G\left(x\right)\right)=\left(x\in I⟼F\left(x\right)\underset{\dot{}}{·}G\left(x\right)\right)$$
29	22 28	eqtrd	$$⊢\phi \to F{\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}G=\left(x\in I⟼F\left(x\right)\underset{\dot{}}{·}G\left(x\right)\right)$$
30	16	fveq2d	$$⊢\phi \to {\cdot }_Y={\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
31	8 30	syl5eq	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
32	31	oveqd	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=F{\cdot }_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}G$$
33		fvexd	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)\in \mathrm{V}$$
34		fvexd	$$⊢\left(\phi \wedge x\in I\right)\to G\left(x\right)\in \mathrm{V}$$
35		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
36	1 35 2 3 4 5	pwselbas	$$⊢\phi \to F:I⟶{\mathrm{Base}}_R$$
37	36	feqmptd	$$⊢\phi \to F=\left(x\in I⟼F\left(x\right)\right)$$
38	1 35 2 3 4 6	pwselbas	$$⊢\phi \to G:I⟶{\mathrm{Base}}_R$$
39	38	feqmptd	$$⊢\phi \to G=\left(x\in I⟼G\left(x\right)\right)$$
40	4 33 34 37 39	offval2	$$⊢\phi \to F{\underset{\dot{}}{·}}_{f}G=\left(x\in I⟼F\left(x\right)\underset{\dot{}}{·}G\left(x\right)\right)$$
41	29 32 40	3eqtr4d	$$⊢\phi \to F\underset{\dot{}}{\bullet }G=F{\underset{\dot{}}{·}}_{f}G$$