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	bitrid	⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 = ℝfld ) ) )