Theorem bj-isrvec2

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-isrvec2.scal	|- ( ph -> ( Scalar ` V ) = K )
2		bj-rvecvec	|- ( V e. RRVec -> V e. LVec )
3	2	a1i	|- ( ph -> ( V e. RRVec -> V e. LVec ) )
4		bj-rvecrr	|- ( V e. RRVec -> ( Scalar ` V ) = RRfld )
5	1	eqeq1d	|- ( ph -> ( ( Scalar ` V ) = RRfld <-> K = RRfld ) )
6	4 5	imbitrid	|- ( ph -> ( V e. RRVec -> K = RRfld ) )
7	3 6	jcad	|- ( ph -> ( V e. RRVec -> ( V e. LVec /\ K = RRfld ) ) )
8		bj-vecssmodel	|- ( V e. LVec -> V e. LMod )
9	8	anim1i	|- ( ( V e. LVec /\ K = RRfld ) -> ( V e. LMod /\ K = RRfld ) )
10	1	bj-isrvecd	|- ( ph -> ( V e. RRVec <-> ( V e. LMod /\ K = RRfld ) ) )
11	9 10	imbitrrid	|- ( ph -> ( ( V e. LVec /\ K = RRfld ) -> V e. RRVec ) )
12	7 11	impbid	|- ( ph -> ( V e. RRVec <-> ( V e. LVec /\ K = RRfld ) ) )