Theorem lsslmod

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

	Ref	Expression
Hypotheses	lsslss.x	|- X = ( W |`s U )
	lsslss.s	|- S = ( LSubSp ` W )
Assertion	lsslmod	|- ( ( W e. LMod /\ U e. S ) -> X e. LMod )

Proof

Step	Hyp	Ref	Expression
1		lsslss.x	|- X = ( W |`s U )
2		lsslss.s	|- S = ( LSubSp ` W )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4	1 3 2	islss3	|- ( W e. LMod -> ( U e. S <-> ( U C_ ( Base ` W ) /\ X e. LMod ) ) )
5	4	simplbda	|- ( ( W e. LMod /\ U e. S ) -> X e. LMod )