Metamath Proof Explorer

Theorem bj-isvec

Description: The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024)

Ref Expression
Hypothesis bj-isvec.scal ⊢φ→K=Scalar⁡V
Assertion bj-isvec ⊢φ→V∈LVec↔V∈LMod∧K∈DivRing

Proof

Step Hyp Ref Expression
1 bj-isvec.scal ⊢φ→K=Scalar⁡V
2 eqid ⊢Scalar⁡V=Scalar⁡V
3 2 islvec ⊢V∈LVec↔V∈LMod∧Scalar⁡V∈DivRing
4 1 eqcomd ⊢φ→Scalar⁡V=K
5 4 eleq1d ⊢φ→Scalar⁡V∈DivRing↔K∈DivRing
6 5 anbi2d ⊢φ→V∈LMod∧Scalar⁡V∈DivRing↔V∈LMod∧K∈DivRing
7 3 6 bitrid ⊢φ→V∈LVec↔V∈LMod∧K∈DivRing