Theorem frlmvscl

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

	Ref	Expression
Hypotheses	frlmvscl.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmvscl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	frlmvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	frlmvscl.m	⊢ · = ( ·𝑠 ‘ 𝐹 )
	frlmvscl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	frlmvscl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	frlmvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	frlmvscl	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		frlmvscl.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmvscl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		frlmvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		frlmvscl.m	⊢ · = ( ·𝑠 ‘ 𝐹 )
5		frlmvscl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		frlmvscl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
7		frlmvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		eqid	⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
9		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
10		reldmfrlm	⊢ Rel dom freeLMod
11	10 1 2	elbasov	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) )
12	7 11	syl	⊢ ( 𝜑 → ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) )
13	12	simprd	⊢ ( 𝜑 → 𝐼 ∈ V )
14	1	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ V ) → 𝐹 ∈ LMod )
15	5 13 14	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ LMod )
16	1	frlmsca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ V ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
17	5 13 16	syl2anc	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
18	17	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
19	3 18	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
20	6 19	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
21	2 8 4 9 15 20 7	lmodvscld	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝐵 )