Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Affine, Euclidean, and Cartesian geometry
Real vector spaces
bj-rvecssmod
Next ⟩
bj-rvecrr
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-rvecssmod
Description:
Real vector spaces are modules.
(Contributed by
BJ
, 6-Jan-2024)
Ref
Expression
Assertion
bj-rvecssmod
⊢
ℝVec
⊆
LMod
Proof
Step
Hyp
Ref
Expression
1
bj-rvecmod
⊢
x
∈
ℝVec
→
x
∈
LMod
2
1
ssriv
⊢
ℝVec
⊆
LMod