Theorem frlmplusgval

Description: Addition in a free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	frlmplusgval.y	$$⊢Y=R\mathrm{freeLMod}I$$
	frlmplusgval.b	$$⊢B={\mathrm{Base}}_Y$$
	frlmplusgval.r	$$⊢\phi \to R\in V$$
	frlmplusgval.i	$$⊢\phi \to I\in W$$
	frlmplusgval.f	$$⊢\phi \to F\in B$$
	frlmplusgval.g	$$⊢\phi \to G\in B$$
	frlmplusgval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	frlmplusgval.p	$$⊢\underset{\dot{}}{✚}={+}_Y$$
Assertion	frlmplusgval	$$⊢\phi \to F\underset{\dot{}}{✚}G=F{\underset{\dot{}}{+}}_{f}G$$

Proof

Step	Hyp	Ref	Expression
1		frlmplusgval.y	$$⊢Y=R\mathrm{freeLMod}I$$
2		frlmplusgval.b	$$⊢B={\mathrm{Base}}_Y$$
3		frlmplusgval.r	$$⊢\phi \to R\in V$$
4		frlmplusgval.i	$$⊢\phi \to I\in W$$
5		frlmplusgval.f	$$⊢\phi \to F\in B$$
6		frlmplusgval.g	$$⊢\phi \to G\in B$$
7		frlmplusgval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
8		frlmplusgval.p	$$⊢\underset{\dot{}}{✚}={+}_Y$$
9		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
10	1 9	frlmpws	$$⊢\left(R\in V\wedge I\in W\right)\to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y$$
11	3 4 10	syl2anc	$$⊢\phi \to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y$$
12	11	fveq2d	$$⊢\phi \to {+}_Y={+}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y\right)}$$
13		fvex	$$⊢{\mathrm{Base}}_Y\in \mathrm{V}$$
14		eqid	$$⊢\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y$$
15		eqid	$$⊢{+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
16	14 15	ressplusg	$$⊢{\mathrm{Base}}_Y\in \mathrm{V}\to {+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={+}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y\right)}$$
17	13 16	ax-mp	$$⊢{+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={+}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_Y\right)}$$
18	12 8 17	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{✚}={+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
19	18	oveqd	$$⊢\phi \to F\underset{\dot{}}{✚}G=F{+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}G$$
20		eqid	$$⊢\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I=\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I$$
21		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
22		fvexd	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{V}$$
23	1 2	frlmpws	$$⊢\left(R\in V\wedge I\in W\right)\to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
24	3 4 23	syl2anc	$$⊢\phi \to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
25	24	fveq2d	$$⊢\phi \to {\mathrm{Base}}_Y={\mathrm{Base}}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
26	2 25	eqtrid	$$⊢\phi \to B={\mathrm{Base}}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
27		eqid	$$⊢\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
28	27 21	ressbasss	$$⊢{\mathrm{Base}}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}\subseteq {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
29	26 28	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
30	29 5	sseldd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
31	29 6	sseldd	$$⊢\phi \to G\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
32		rlmplusg	$$⊢{+}_R={+}_{\mathrm{ringLMod}\left(R\right)}$$
33	7 32	eqtri	$$⊢\underset{\dot{}}{+}={+}_{\mathrm{ringLMod}\left(R\right)}$$
34	20 21 22 4 30 31 33 15	pwsplusgval	$$⊢\phi \to F{+}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}G=F{\underset{\dot{}}{+}}_{f}G$$
35	19 34	eqtrd	$$⊢\phi \to F\underset{\dot{}}{✚}G=F{\underset{\dot{}}{+}}_{f}G$$