Theorem frlmvscl

Description: Closure of scalar multiplication in a free module. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Hypotheses	frlmvscl.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmvscl.b	$$⊢B={\mathrm{Base}}_F$$
	frlmvscl.k	$$⊢K={\mathrm{Base}}_R$$
	frlmvscl.m	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
	frlmvscl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	frlmvscl.a	$$⊢\phi \to A\in K$$
	frlmvscl.x	$$⊢\phi \to X\in B$$
Assertion	frlmvscl	$$⊢\phi \to A\underset{\dot{}}{·}X\in B$$

Proof

Step	Hyp	Ref	Expression
1		frlmvscl.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmvscl.b	$$⊢B={\mathrm{Base}}_F$$
3		frlmvscl.k	$$⊢K={\mathrm{Base}}_R$$
4		frlmvscl.m	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
5		frlmvscl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		frlmvscl.a	$$⊢\phi \to A\in K$$
7		frlmvscl.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢\mathrm{Scalar}\left(F\right)=\mathrm{Scalar}\left(F\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
10		reldmfrlm	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{freeLMod}$$
11	10 1 2	elbasov	$$⊢X\in B\to \left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)$$
12	7 11	syl	$$⊢\phi \to \left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)$$
13	12	simprd	$$⊢\phi \to I\in \mathrm{V}$$
14	1	frlmlmod	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{V}\right)\to F\in \mathrm{LMod}$$
15	5 13 14	syl2anc	$$⊢\phi \to F\in \mathrm{LMod}$$
16	1	frlmsca	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{V}\right)\to R=\mathrm{Scalar}\left(F\right)$$
17	5 13 16	syl2anc	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$
18	17	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
19	3 18	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
20	6 19	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
21	2 8 4 9 15 20 7	lmodvscld	$$⊢\phi \to A\underset{\dot{}}{·}X\in B$$