Metamath Proof Explorer

Theorem aspid

Description: The algebraic span of a subalgebra is itself. ( spanid analog.) (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 aspid 
|- ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> ( A ` S ) = S )

Proof

Step Hyp Ref Expression
1 aspval.a 
 |-  A = ( AlgSpan ` W )
2 aspval.v 
 |-  V = ( Base ` W )
3 aspval.l 
 |-  L = ( LSubSp ` W )
4 simp1 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> W e. AssAlg )
5 2 subrgss 
 |-  ( S e. ( SubRing ` W ) -> S C_ V )
6 5 3ad2ant2 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> S C_ V )
7 1 2 3 aspval 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )
8 4 6 7 syl2anc 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )
9 3simpc 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> ( S e. ( SubRing ` W ) /\ S e. L ) )
10 elin 
 |-  ( S e. ( ( SubRing ` W ) i^i L ) <-> ( S e. ( SubRing ` W ) /\ S e. L ) )
11 9 10 sylibr 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> S e. ( ( SubRing ` W ) i^i L ) )
12 intmin 
 |-  ( S e. ( ( SubRing ` W ) i^i L ) -> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } = S )
13 11 12 syl 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } = S )
14 8 13 eqtrd 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) /\ S e. L ) -> ( A ` S ) = S )