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