This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )