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

Proof

Step Hyp Ref Expression
1 bj-isrvecd.scal ( 𝜑 → ( Scalar ‘ 𝑉 ) = 𝐾 )
2 bj-isrvec ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) )
3 1 eqeq1d ( 𝜑 → ( ( Scalar ‘ 𝑉 ) = ℝfld𝐾 = ℝfld ) )
4 3 anbi2d ( 𝜑 → ( ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) = ℝfld ) ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) )
5 2 4 syl5bb ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) )