Theorem frlmvscafval

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

	Ref	Expression
Hypotheses	frlmvscafval.y	$$⊢Y=R\mathrm{freeLMod}I$$
	frlmvscafval.b	$$⊢B={\mathrm{Base}}_Y$$
	frlmvscafval.k	$$⊢K={\mathrm{Base}}_R$$
	frlmvscafval.i	$$⊢\phi \to I\in W$$
	frlmvscafval.a	$$⊢\phi \to A\in K$$
	frlmvscafval.x	$$⊢\phi \to X\in B$$
	frlmvscafval.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
	frlmvscafval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	frlmvscafval	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X$$

Proof

Step	Hyp	Ref	Expression
1		frlmvscafval.y	$$⊢Y=R\mathrm{freeLMod}I$$
2		frlmvscafval.b	$$⊢B={\mathrm{Base}}_Y$$
3		frlmvscafval.k	$$⊢K={\mathrm{Base}}_R$$
4		frlmvscafval.i	$$⊢\phi \to I\in W$$
5		frlmvscafval.a	$$⊢\phi \to A\in K$$
6		frlmvscafval.x	$$⊢\phi \to X\in B$$
7		frlmvscafval.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
8		frlmvscafval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
9	1 2	frlmrcl	$$⊢X\in B\to R\in \mathrm{V}$$
10	6 9	syl	$$⊢\phi \to R\in \mathrm{V}$$
11	1 2	frlmpws	$$⊢\left(R\in \mathrm{V}\wedge I\in W\right)\to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
12	10 4 11	syl2anc	$$⊢\phi \to Y=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
13	12	fveq2d	$$⊢\phi \to {\cdot }_Y={\cdot }_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
14	2	fvexi	$$⊢B\in \mathrm{V}$$
15		eqid	$$⊢\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B=\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B$$
16		eqid	$$⊢{\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
17	15 16	ressvsca	$$⊢B\in \mathrm{V}\to {\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={\cdot }_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
18	14 17	ax-mp	$$⊢{\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={\cdot }_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
19	13 7 18	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
20	19	oveqd	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=A{\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}X$$
21		eqid	$$⊢\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I=\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I$$
22		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}={\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
23		rlmvsca	$$⊢{\cdot }_R={\cdot }_{\mathrm{ringLMod}\left(R\right)}$$
24	8 23	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{ringLMod}\left(R\right)}$$
25		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
26		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
27		fvexd	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{V}$$
28		rlmsca	$$⊢R\in \mathrm{V}\to R=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
29	10 28	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)$$
30	29	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
31	3 30	syl5eq	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
32	5 31	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{ringLMod}\left(R\right)\right)}$$
33	12	fveq2d	$$⊢\phi \to {\mathrm{Base}}_Y={\mathrm{Base}}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
34	2 33	syl5eq	$$⊢\phi \to B={\mathrm{Base}}_{\left(\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right){\upharpoonright }_{𝑠}B\right)}$$
35	15 22	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)}$$
36	34 35	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
37	36 6	sseldd	$$⊢\phi \to X\in {\mathrm{Base}}_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}$$
38	21 22 24 16 25 26 27 4 32 37	pwsvscafval	$$⊢\phi \to A{\cdot }_{\left(\mathrm{ringLMod}\left(R\right){\uparrow }_{𝑠}I\right)}X=\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X$$
39	20 38	eqtrd	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=\left(I\times \left\{A\right\}\right){\underset{\dot{}}{·}}_{f}X$$