Theorem fglmod

Description: Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Assertion	fglmod	$$⊢M\in \mathrm{LFinGen}\to M\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		df-lfig	$$⊢\mathrm{LFinGen}=\left\{a\in \mathrm{LMod}|{\mathrm{Base}}_a\in \mathrm{LSpan}\left(a\right)\left[𝒫{\mathrm{Base}}_a\cap \mathrm{Fin}\right]\right\}$$
2	1	ssrab3	$$⊢\mathrm{LFinGen}\subseteq \mathrm{LMod}$$
3	2	sseli	$$⊢M\in \mathrm{LFinGen}\to M\in \mathrm{LMod}$$