Metamath Proof Explorer

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 imbitrid ⊢ φ → 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 imbitrrid ⊢ φ → V ∈ LVec ∧ K = ℝ fld → V ∈ ℝVec
12 7 11 impbid ⊢ φ → V ∈ ℝVec ↔ V ∈ LVec ∧ K = ℝ fld