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	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspssp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	lspssp	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑇 ) ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lspssp.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lspssp.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4	3 1	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
5	3 2	lspss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ 𝑈 ) )
6	4 5	syl3an2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ 𝑈 ) )
7	1 2	lspid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ 𝑈 ) = 𝑈 )
8	7	3adant3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑈 ) = 𝑈 )
9	6 8	sseqtrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑇 ) ⊆ 𝑈 )