Theorem aspsubrg

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

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

Proof

Step	Hyp	Ref	Expression
1		aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2		aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
4	1 2 3	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } )
5		ssrab2	⊢ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ⊆ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) )
6		inss1	⊢ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ⊆ ( SubRing ‘ 𝑊 )
7	5 6	sstri	⊢ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ⊆ ( SubRing ‘ 𝑊 )
8		fvex	⊢ ( 𝐴 ‘ 𝑆 ) ∈ V
9	4 8	eqeltrrdi	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ∈ V )
10		intex	⊢ ( { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ≠ ∅ ↔ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ∈ V )
11	9 10	sylibr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ≠ ∅ )
12		subrgint	⊢ ( ( { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ⊆ ( SubRing ‘ 𝑊 ) ∧ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ≠ ∅ ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ∈ ( SubRing ‘ 𝑊 ) )
13	7 11 12	sylancr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ∈ ( SubRing ‘ 𝑊 ) )
14	4 13	eqeltrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) ∈ ( SubRing ‘ 𝑊 ) )