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