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