This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) ∈ 𝐿 )