Theorem bj-isvec

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

	Ref	Expression
Hypothesis	bj-isvec.scal	⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑉 ) )
Assertion	bj-isvec	⊢ ( 𝜑 → ( 𝑉 ∈ LVec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-isvec.scal	⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑉 ) )
2		eqid	⊢ ( Scalar ‘ 𝑉 ) = ( Scalar ‘ 𝑉 )
3	2	islvec	⊢ ( 𝑉 ∈ LVec ↔ ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) ∈ DivRing ) )
4	1	eqcomd	⊢ ( 𝜑 → ( Scalar ‘ 𝑉 ) = 𝐾 )
5	4	eleq1d	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑉 ) ∈ DivRing ↔ 𝐾 ∈ DivRing ) )
6	5	anbi2d	⊢ ( 𝜑 → ( ( 𝑉 ∈ LMod ∧ ( Scalar ‘ 𝑉 ) ∈ DivRing ) ↔ ( 𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing ) ) )
7	3 6	bitrid	⊢ ( 𝜑 → ( 𝑉 ∈ LVec ↔ ( 𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing ) ) )