Theorem bj-rvecvec

Description: Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024)

	Ref	Expression
Assertion	bj-rvecvec	|- ( V e. RRVec -> V e. LVec )

Proof

Step	Hyp	Ref	Expression
1		bj-rvecmod	|- ( V e. RRVec -> V e. LMod )
2		bj-rrdrg	|- RRfld e. DivRing
3	2	a1i	|- ( V e. RRVec -> RRfld e. DivRing )
4		bj-rvecrr	|- ( V e. RRVec -> ( Scalar ` V ) = RRfld )
5	4	eqcomd	|- ( V e. RRVec -> RRfld = ( Scalar ` V ) )
6	5	bj-isvec	|- ( V e. RRVec -> ( V e. LVec <-> ( V e. LMod /\ RRfld e. DivRing ) ) )
7	1 3 6	mpbir2and	|- ( V e. RRVec -> V e. LVec )