Theorem lspssid

Description: A set of vectors is a subset of its span. ( spanss2 analog.) (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspss.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	lspssid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lspss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspss.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		ssintub	⊢ 𝑈 ⊆ ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈 ⊆ 𝑡 }
4		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
5	1 4 2	lspval	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑈 ) = ∩ { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈 ⊆ 𝑡 } )
6	3 5	sseqtrrid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 ⊆ ( 𝑁 ‘ 𝑈 ) )