Theorem pwsplusgval

Description: Value of addition 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$$
	pwsplusgval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	pwsplusgval.p	$$⊢\underset{\dot{}}{✚}={+}_Y$$
Assertion	pwsplusgval	$$⊢\phi \to F\underset{\dot{}}{✚}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		pwsplusgval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
8		pwsplusgval.p	$$⊢\underset{\dot{}}{✚}={+}_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	eqtrid	$$⊢\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	$$⊢{+}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}={+}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
22	9 10 11 4 13 19 20 21	prdsplusgval	$$⊢\phi \to F{+}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}G=\left(x\in I⟼F\left(x\right){+}_{\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 {+}_{\left(I\times \left\{R\right\}\right)\left(x\right)}={+}_R$$
26	25 7	eqtr4di	$$⊢\left(\phi \wedge x\in I\right)\to {+}_{\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){+}_{\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){+}_{\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{+}_{\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 {+}_Y={+}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
31	8 30	eqtrid	$$⊢\phi \to \underset{\dot{}}{✚}={+}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)}$$
32	31	oveqd	$$⊢\phi \to F\underset{\dot{}}{✚}G=F{+}_{\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{}}{✚}G=F{\underset{\dot{}}{+}}_{f}G$$