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