Metamath Proof Explorer

Theorem lvecring

Description: The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023)

Ref Expression
Hypothesis lvecring.1 
|- F = ( Scalar ` W )
Assertion lvecring 
|- ( W e. LVec -> F e. Ring )

Proof

Step Hyp Ref Expression
1 lvecring.1 
 |-  F = ( Scalar ` W )
2 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
3 1 lmodring 
 |-  ( W e. LMod -> F e. Ring )
4 2 3 syl 
 |-  ( W e. LVec -> F e. Ring )