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 A=AlgSpanW
aspval.v V=BaseW
aspval.l L=LSubSpW
Assertion asplss WAssAlgSVASL

Proof

Step Hyp Ref Expression
1 aspval.a A=AlgSpanW
2 aspval.v V=BaseW
3 aspval.l L=LSubSpW
4 1 2 3 aspval WAssAlgSVAS=tSubRingWL|St
5 assalmod WAssAlgWLMod
6 5 adantr WAssAlgSVWLMod
7 ssrab2 tSubRingWL|StSubRingWL
8 inss2 SubRingWLL
9 7 8 sstri tSubRingWL|StL
10 9 a1i WAssAlgSVtSubRingWL|StL
11 fvex ASV
12 4 11 eqeltrrdi WAssAlgSVtSubRingWL|StV
13 intex tSubRingWL|SttSubRingWL|StV
14 12 13 sylibr WAssAlgSVtSubRingWL|St
15 3 lssintcl WLModtSubRingWL|StLtSubRingWL|SttSubRingWL|StL
16 6 10 14 15 syl3anc WAssAlgSVtSubRingWL|StL
17 4 16 eqeltrd WAssAlgSVASL