Description: The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lvecring.1 | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | |
Assertion | lvecring | ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ Ring ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lvecring.1 | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | |
2 | lveclmod | ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod ) | |
3 | 1 | lmodring | ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring ) |
4 | 2 3 | syl | ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ Ring ) |