Theorem asplss

Description: The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2		aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		aspval.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4	1 2 3	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )
5		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
6	5	adantr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → 𝑊 ∈ LMod )
7		ssrab2	⊢ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ⊆ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 )
8		inss2	⊢ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ⊆ 𝐿
9	7 8	sstri	⊢ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ⊆ 𝐿
10	9	a1i	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ⊆ 𝐿 )
11		fvex	⊢ ( 𝐴 ‘ 𝑆 ) ∈ V
12	4 11	eqeltrrdi	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ∈ V )
13		intex	⊢ ( { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ≠ ∅ ↔ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ∈ V )
14	12 13	sylibr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ≠ ∅ )
15	3	lssintcl	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ⊆ 𝐿 ∧ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ≠ ∅ ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ∈ 𝐿 )
16	6 10 14 15	syl3anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ∈ 𝐿 )
17	4 16	eqeltrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) ∈ 𝐿 )