Theorem lvecisfrlm

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

	Ref	Expression
Hypothesis	lvecisfrlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	lvecisfrlm	⊢ ( 𝑊 ∈ LVec → ∃ 𝑘 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		lvecisfrlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		eqid	⊢ ( LBasis ‘ 𝑊 ) = ( LBasis ‘ 𝑊 )
3	2	lbsex	⊢ ( 𝑊 ∈ LVec → ( LBasis ‘ 𝑊 ) ≠ ∅ )
4		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
5	2 1	lmisfree	⊢ ( 𝑊 ∈ LMod → ( ( LBasis ‘ 𝑊 ) ≠ ∅ ↔ ∃ 𝑘 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝑘 ) ) )
6	4 5	syl	⊢ ( 𝑊 ∈ LVec → ( ( LBasis ‘ 𝑊 ) ≠ ∅ ↔ ∃ 𝑘 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝑘 ) ) )
7	3 6	mpbid	⊢ ( 𝑊 ∈ LVec → ∃ 𝑘 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝑘 ) )