Theorem lvecisfrlm

Description: Every vector space is isomorphic to a free module. (Contributed by AV, 7-Mar-2019)

	Ref	Expression
Hypothesis	lvecisfrlm.f	|- F = ( Scalar ` W )
Assertion	lvecisfrlm	|- ( W e. LVec -> E. k W ~=m ( F freeLMod k ) )

Proof

Step	Hyp	Ref	Expression
1		lvecisfrlm.f	|- F = ( Scalar ` W )
2		eqid	|- ( LBasis ` W ) = ( LBasis ` W )
3	2	lbsex	|- ( W e. LVec -> ( LBasis ` W ) =/= (/) )
4		lveclmod	|- ( W e. LVec -> W e. LMod )
5	2 1	lmisfree	|- ( W e. LMod -> ( ( LBasis ` W ) =/= (/) <-> E. k W ~=m ( F freeLMod k ) ) )
6	4 5	syl	|- ( W e. LVec -> ( ( LBasis ` W ) =/= (/) <-> E. k W ~=m ( F freeLMod k ) ) )
7	3 6	mpbid	|- ( W e. LVec -> E. k W ~=m ( F freeLMod k ) )