Theorem lsslmod

Description: A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014)

	Ref	Expression
Hypotheses	lsslss.x	$$⊢X=W{\upharpoonright }_{𝑠}U$$
	lsslss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lsslmod	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to X\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		lsslss.x	$$⊢X=W{\upharpoonright }_{𝑠}U$$
2		lsslss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4	1 3 2	islss3	$$⊢W\in \mathrm{LMod}\to \left(U\in S\leftrightarrow \left(U\subseteq {\mathrm{Base}}_W\wedge X\in \mathrm{LMod}\right)\right)$$
5	4	simplbda	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to X\in \mathrm{LMod}$$