Metamath Proof Explorer

Theorem aspval

Description: Value of the algebraic closure operation inside an associative algebra. (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 aspval 
|- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )

Proof

Step Hyp Ref Expression
1 aspval.a 
 |-  A = ( AlgSpan ` W )
2 aspval.v 
 |-  V = ( Base ` W )
3 aspval.l 
 |-  L = ( LSubSp ` W )
4 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
5 4 2 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
6 5 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P V )
7 fveq2 
 |-  ( w = W -> ( SubRing ` w ) = ( SubRing ` W ) )
8 fveq2 
 |-  ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
9 8 3 eqtr4di 
 |-  ( w = W -> ( LSubSp ` w ) = L )
10 7 9 ineq12d 
 |-  ( w = W -> ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) = ( ( SubRing ` W ) i^i L ) )
11 10 rabeqdv 
 |-  ( w = W -> { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } = { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } )
12 11 inteqd 
 |-  ( w = W -> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } = |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } )
13 6 12 mpteq12dv 
 |-  ( w = W -> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) = ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) )
14 df-asp 
 |-  AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( ( SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
15 2 fvexi 
 |-  V e. _V
16 15 pwex 
 |-  ~P V e. _V
17 16 mptex 
 |-  ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) e. _V
18 13 14 17 fvmpt 
 |-  ( W e. AssAlg -> ( AlgSpan ` W ) = ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) )
19 1 18 syl5eq 
 |-  ( W e. AssAlg -> A = ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) )
20 19 fveq1d 
 |-  ( W e. AssAlg -> ( A ` S ) = ( ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) ` S ) )
21 20 adantr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = ( ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) ` S ) )
22 eqid 
 |-  ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) = ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } )
23 sseq1 
 |-  ( s = S -> ( s C_ t <-> S C_ t ) )
24 23 rabbidv 
 |-  ( s = S -> { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } = { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )
25 24 inteqd 
 |-  ( s = S -> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )
26 simpr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> S C_ V )
27 15 elpw2 
 |-  ( S e. ~P V <-> S C_ V )
28 26 27 sylibr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> S e. ~P V )
29 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
30 2 subrgid 
 |-  ( W e. Ring -> V e. ( SubRing ` W ) )
31 29 30 syl 
 |-  ( W e. AssAlg -> V e. ( SubRing ` W ) )
32 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
33 2 3 lss1 
 |-  ( W e. LMod -> V e. L )
34 32 33 syl 
 |-  ( W e. AssAlg -> V e. L )
35 31 34 elind 
 |-  ( W e. AssAlg -> V e. ( ( SubRing ` W ) i^i L ) )
36 sseq2 
 |-  ( t = V -> ( S C_ t <-> S C_ V ) )
37 36 rspcev 
 |-  ( ( V e. ( ( SubRing ` W ) i^i L ) /\ S C_ V ) -> E. t e. ( ( SubRing ` W ) i^i L ) S C_ t )
38 35 37 sylan 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> E. t e. ( ( SubRing ` W ) i^i L ) S C_ t )
39 intexrab 
 |-  ( E. t e. ( ( SubRing ` W ) i^i L ) S C_ t <-> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } e. _V )
40 38 39 sylib 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } e. _V )
41 22 25 28 40 fvmptd3 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( ( s e. ~P V |-> |^| { t e. ( ( SubRing ` W ) i^i L ) | s C_ t } ) ` S ) = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )
42 21 41 eqtrd 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { t e. ( ( SubRing ` W ) i^i L ) | S C_ t } )