Metamath Proof Explorer

Theorem bj-isrvecd

Description: The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024)

Ref Expression
Hypothesis bj-isrvecd.scal ⊢φ→Scalar⁡V=K
Assertion bj-isrvecd ⊢φ→V∈ℝVec↔V∈LMod∧K=ℝfld

Proof

Step Hyp Ref Expression
1 bj-isrvecd.scal ⊢φ→Scalar⁡V=K
2 bj-isrvec ⊢V∈ℝVec↔V∈LMod∧Scalar⁡V=ℝfld
3 1 eqeq1d ⊢φ→Scalar⁡V=ℝfld↔K=ℝfld
4 3 anbi2d ⊢φ→V∈LMod∧Scalar⁡V=ℝfld↔V∈LMod∧K=ℝfld
5 2 4 bitrid ⊢φ→V∈ℝVec↔V∈LMod∧K=ℝfld