Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 aspval.a 
 |-  A = ( AlgSpan ` W )
2 aspval.v 
 |-  V = ( Base ` W )
3 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
4 1 2 3 aspval 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } )
5 ssrab2 
 |-  { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } C_ ( ( SubRing ` W ) i^i ( LSubSp ` W ) )
6 inss1 
 |-  ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) C_ ( SubRing ` W )
7 5 6 sstri 
 |-  { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } C_ ( SubRing ` W )
8 fvex 
 |-  ( A ` S ) e. _V
9 4 8 eqeltrrdi 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } e. _V )
10 intex 
 |-  ( { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } =/= (/) <-> |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } e. _V )
11 9 10 sylibr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } =/= (/) )
12 subrgint 
 |-  ( ( { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } C_ ( SubRing ` W ) /\ { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } =/= (/) ) -> |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } e. ( SubRing ` W ) )
13 7 11 12 sylancr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> |^| { t e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ t } e. ( SubRing ` W ) )
14 4 13 eqeltrd 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) e. ( SubRing ` W ) )