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 = ( AlgSpan ` W )
aspval.v 
|- V = ( Base ` W )
aspval.l 
|- L = ( LSubSp ` W )
Assertion asplss 
|- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) e. L )

Proof

Step Hyp Ref Expression
1 aspval.a 
 |-  A = ( AlgSpan ` W )
2 aspval.v 
 |-  V = ( Base ` W )
3 aspval.l 
 |-  L = ( LSubSp ` W )
4 1 2 3 aspval 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )
5 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
6 5 adantr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> W e. LMod )
7 ssrab2 
 |-  { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } C_ ( ( SubRing ` W ) i^i L )
8 inss2 
 |-  ( ( SubRing ` W ) i^i L ) C_ L
9 7 8 sstri 
 |-  { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } C_ L
10 9 a1i 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } C_ L )
11 fvex 
 |-  ( A ` S ) e. _V
12 4 11 eqeltrrdi 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } e. _V )
13 intex 
 |-  ( { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } =/= (/) <-> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } e. _V )
14 12 13 sylibr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } =/= (/) )
15 3 lssintcl 
 |-  ( ( W e. LMod /\ { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } C_ L /\ { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } =/= (/) ) -> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } e. L )
16 6 10 14 15 syl3anc 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } e. L )
17 4 16 eqeltrd 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) e. L )