Metamath Proof Explorer

Theorem frlmvscl

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

Ref Expression
Hypotheses frlmvscl.f 
|- F = ( R freeLMod I )
frlmvscl.b 
|- B = ( Base ` F )
frlmvscl.k 
|- K = ( Base ` R )
frlmvscl.m 
|- .x. = ( .s ` F )
frlmvscl.r 
|- ( ph -> R e. Ring )
frlmvscl.a 
|- ( ph -> A e. K )
frlmvscl.x 
|- ( ph -> X e. B )
Assertion frlmvscl 
|- ( ph -> ( A .x. X ) e. B )

Proof

Step Hyp Ref Expression
1 frlmvscl.f 
 |-  F = ( R freeLMod I )
2 frlmvscl.b 
 |-  B = ( Base ` F )
3 frlmvscl.k 
 |-  K = ( Base ` R )
4 frlmvscl.m 
 |-  .x. = ( .s ` F )
5 frlmvscl.r 
 |-  ( ph -> R e. Ring )
6 frlmvscl.a 
 |-  ( ph -> A e. K )
7 frlmvscl.x 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( Scalar ` F ) = ( Scalar ` F )
9 eqid 
 |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )
10 reldmfrlm 
 |-  Rel dom freeLMod
11 10 1 2 elbasov 
 |-  ( X e. B -> ( R e. _V /\ I e. _V ) )
12 7 11 syl 
 |-  ( ph -> ( R e. _V /\ I e. _V ) )
13 12 simprd 
 |-  ( ph -> I e. _V )
14 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. _V ) -> F e. LMod )
15 5 13 14 syl2anc 
 |-  ( ph -> F e. LMod )
16 1 frlmsca 
 |-  ( ( R e. Ring /\ I e. _V ) -> R = ( Scalar ` F ) )
17 5 13 16 syl2anc 
 |-  ( ph -> R = ( Scalar ` F ) )
18 17 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
19 3 18 eqtrid 
 |-  ( ph -> K = ( Base ` ( Scalar ` F ) ) )
20 6 19 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` F ) ) )
21 2 8 4 9 15 20 7 lmodvscld 
 |-  ( ph -> ( A .x. X ) e. B )