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 ‘ 𝑉 ) = 𝐾 )
Assertion bj-isrvec2 ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) ) )

Proof

Step Hyp Ref Expression
1 bj-isrvec2.scal ( 𝜑 → ( Scalar ‘ 𝑉 ) = 𝐾 )
2 bj-rvecvec ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec )
3 2 a1i ( 𝜑 → ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec ) )
4 bj-rvecrr ( 𝑉 ∈ ℝ-Vec → ( Scalar ‘ 𝑉 ) = ℝfld )
5 1 eqeq1d ( 𝜑 → ( ( Scalar ‘ 𝑉 ) = ℝfld𝐾 = ℝfld ) )
6 4 5 syl5ib ( 𝜑 → ( 𝑉 ∈ ℝ-Vec → 𝐾 = ℝfld ) )
7 3 6 jcad ( 𝜑 → ( 𝑉 ∈ ℝ-Vec → ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) ) )
8 bj-vecssmodel ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
9 8 anim1i ( ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) → ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) )
10 1 bj-isrvecd ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) )
11 9 10 syl5ibr ( 𝜑 → ( ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) → 𝑉 ∈ ℝ-Vec ) )
12 7 11 impbid ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) ) )