Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Affine, Euclidean, and Cartesian geometry
Real vector spaces
bj-isrvec2
Next ⟩
bj-rvecssvec
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-isrvec2
Description:
The predicate "is a real vector space".
(Contributed by
BJ
, 6-Jan-2024)
Ref
Expression
Hypothesis
bj-isrvec2.scal
⊢
φ
→
Scalar
⁡
V
=
K
Assertion
bj-isrvec2
⊢
φ
→
V
∈
ℝVec
↔
V
∈
LVec
∧
K
=
ℝ
fld
Proof
Step
Hyp
Ref
Expression
1
bj-isrvec2.scal
⊢
φ
→
Scalar
⁡
V
=
K
2
bj-rvecvec
⊢
V
∈
ℝVec
→
V
∈
LVec
3
2
a1i
⊢
φ
→
V
∈
ℝVec
→
V
∈
LVec
4
bj-rvecrr
⊢
V
∈
ℝVec
→
Scalar
⁡
V
=
ℝ
fld
5
1
eqeq1d
⊢
φ
→
Scalar
⁡
V
=
ℝ
fld
↔
K
=
ℝ
fld
6
4
5
syl5ib
⊢
φ
→
V
∈
ℝVec
→
K
=
ℝ
fld
7
3
6
jcad
⊢
φ
→
V
∈
ℝVec
→
V
∈
LVec
∧
K
=
ℝ
fld
8
bj-vecssmodel
⊢
V
∈
LVec
→
V
∈
LMod
9
8
anim1i
⊢
V
∈
LVec
∧
K
=
ℝ
fld
→
V
∈
LMod
∧
K
=
ℝ
fld
10
1
bj-isrvecd
⊢
φ
→
V
∈
ℝVec
↔
V
∈
LMod
∧
K
=
ℝ
fld
11
9
10
syl5ibr
⊢
φ
→
V
∈
LVec
∧
K
=
ℝ
fld
→
V
∈
ℝVec
12
7
11
impbid
⊢
φ
→
V
∈
ℝVec
↔
V
∈
LVec
∧
K
=
ℝ
fld