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	imbitrid	⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-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	imbitrrid	⊢ ( 𝜑 → ( ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) → 𝑉 ∈ ℝ-Vec ) )
12	7 11	impbid	⊢ ( 𝜑 → ( 𝑉 ∈ ℝ-Vec ↔ ( 𝑉 ∈ LVec ∧ 𝐾 = ℝfld ) ) )