Theorem lspssp

Description: If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014)

	Ref	Expression
Hypotheses	lspssp.s	|- S = ( LSubSp ` W )
	lspssp.n	|- N = ( LSpan ` W )
Assertion	lspssp	|- ( ( W e. LMod /\ U e. S /\ T C_ U ) -> ( N ` T ) C_ U )

Proof

Step	Hyp	Ref	Expression
1		lspssp.s	|- S = ( LSubSp ` W )
2		lspssp.n	|- N = ( LSpan ` W )
3		eqid	|- ( Base ` W ) = ( Base ` W )
4	3 1	lssss	|- ( U e. S -> U C_ ( Base ` W ) )
5	3 2	lspss	|- ( ( W e. LMod /\ U C_ ( Base ` W ) /\ T C_ U ) -> ( N ` T ) C_ ( N ` U ) )
6	4 5	syl3an2	|- ( ( W e. LMod /\ U e. S /\ T C_ U ) -> ( N ` T ) C_ ( N ` U ) )
7	1 2	lspid	|- ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U )
8	7	3adant3	|- ( ( W e. LMod /\ U e. S /\ T C_ U ) -> ( N ` U ) = U )
9	6 8	sseqtrd	|- ( ( W e. LMod /\ U e. S /\ T C_ U ) -> ( N ` T ) C_ U )