Theorem bj-isvec

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

	Ref	Expression
Hypothesis	bj-isvec.scal	|- ( ph -> K = ( Scalar ` V ) )
Assertion	bj-isvec	|- ( ph -> ( V e. LVec <-> ( V e. LMod /\ K e. DivRing ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-isvec.scal	|- ( ph -> K = ( Scalar ` V ) )
2		eqid	|- ( Scalar ` V ) = ( Scalar ` V )
3	2	islvec	|- ( V e. LVec <-> ( V e. LMod /\ ( Scalar ` V ) e. DivRing ) )
4	1	eqcomd	|- ( ph -> ( Scalar ` V ) = K )
5	4	eleq1d	|- ( ph -> ( ( Scalar ` V ) e. DivRing <-> K e. DivRing ) )
6	5	anbi2d	|- ( ph -> ( ( V e. LMod /\ ( Scalar ` V ) e. DivRing ) <-> ( V e. LMod /\ K e. DivRing ) ) )
7	3 6	bitrid	|- ( ph -> ( V e. LVec <-> ( V e. LMod /\ K e. DivRing ) ) )