Theorem bj-isrvecd

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

	Ref	Expression
Hypothesis	bj-isrvecd.scal	|- ( ph -> ( Scalar ` V ) = K )
Assertion	bj-isrvecd	|- ( ph -> ( V e. RRVec <-> ( V e. LMod /\ K = RRfld ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-isrvecd.scal	|- ( ph -> ( Scalar ` V ) = K )
2		bj-isrvec	|- ( V e. RRVec <-> ( V e. LMod /\ ( Scalar ` V ) = RRfld ) )
3	1	eqeq1d	|- ( ph -> ( ( Scalar ` V ) = RRfld <-> K = RRfld ) )
4	3	anbi2d	|- ( ph -> ( ( V e. LMod /\ ( Scalar ` V ) = RRfld ) <-> ( V e. LMod /\ K = RRfld ) ) )
5	2 4	syl5bb	|- ( ph -> ( V e. RRVec <-> ( V e. LMod /\ K = RRfld ) ) )