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	⊢ 𝑆 = ( 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 ∧ 𝑈 ∈ 𝑆 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑇 ) ⊆ 𝑈 )