Theorem aspssid

Description: A set of vectors is a subset of its span. ( spanss2 analog.) (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
	aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion	aspssid	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( 𝐴 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2		aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		ssintub	⊢ 𝑆 ⊆ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 }
4		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
5	1 2 4	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } )
6	3 5	sseqtrrid	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( 𝐴 ‘ 𝑆 ) )