Metamath Proof Explorer

Theorem aspval2

Description: The algebraic closure is the ring closure when the generating set is expanded to include all scalars.EDITORIAL : In light of this, is AlgSpan independently needed? (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypotheses aspval2.a 
|- A = ( AlgSpan ` W )
aspval2.c 
|- C = ( algSc ` W )
aspval2.r 
|- R = ( mrCls ` ( SubRing ` W ) )
aspval2.v 
|- V = ( Base ` W )
Assertion aspval2 
|- ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = ( R ` ( ran C u. S ) ) )

Proof

Step Hyp Ref Expression
1 aspval2.a 
 |-  A = ( AlgSpan ` W )
2 aspval2.c 
 |-  C = ( algSc ` W )
3 aspval2.r 
 |-  R = ( mrCls ` ( SubRing ` W ) )
4 aspval2.v 
 |-  V = ( Base ` W )
5 elin 
 |-  ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) <-> ( x e. ( SubRing ` W ) /\ x e. ( LSubSp ` W ) ) )
6 5 anbi1i 
 |-  ( ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) /\ S C_ x ) <-> ( ( x e. ( SubRing ` W ) /\ x e. ( LSubSp ` W ) ) /\ S C_ x ) )
7 anass 
 |-  ( ( ( x e. ( SubRing ` W ) /\ x e. ( LSubSp ` W ) ) /\ S C_ x ) <-> ( x e. ( SubRing ` W ) /\ ( x e. ( LSubSp ` W ) /\ S C_ x ) ) )
8 6 7 bitri 
 |-  ( ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) /\ S C_ x ) <-> ( x e. ( SubRing ` W ) /\ ( x e. ( LSubSp ` W ) /\ S C_ x ) ) )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 2 9 issubassa2 
 |-  ( ( W e. AssAlg /\ x e. ( SubRing ` W ) ) -> ( x e. ( LSubSp ` W ) <-> ran C C_ x ) )
11 10 anbi1d 
 |-  ( ( W e. AssAlg /\ x e. ( SubRing ` W ) ) -> ( ( x e. ( LSubSp ` W ) /\ S C_ x ) <-> ( ran C C_ x /\ S C_ x ) ) )
12 unss 
 |-  ( ( ran C C_ x /\ S C_ x ) <-> ( ran C u. S ) C_ x )
13 11 12 bitrdi 
 |-  ( ( W e. AssAlg /\ x e. ( SubRing ` W ) ) -> ( ( x e. ( LSubSp ` W ) /\ S C_ x ) <-> ( ran C u. S ) C_ x ) )
14 13 pm5.32da 
 |-  ( W e. AssAlg -> ( ( x e. ( SubRing ` W ) /\ ( x e. ( LSubSp ` W ) /\ S C_ x ) ) <-> ( x e. ( SubRing ` W ) /\ ( ran C u. S ) C_ x ) ) )
15 8 14 bitrid 
 |-  ( W e. AssAlg -> ( ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) /\ S C_ x ) <-> ( x e. ( SubRing ` W ) /\ ( ran C u. S ) C_ x ) ) )
16 15 abbidv 
 |-  ( W e. AssAlg -> { x | ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) /\ S C_ x ) } = { x | ( x e. ( SubRing ` W ) /\ ( ran C u. S ) C_ x ) } )
17 16 adantr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> { x | ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) /\ S C_ x ) } = { x | ( x e. ( SubRing ` W ) /\ ( ran C u. S ) C_ x ) } )
18 df-rab 
 |-  { x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ x } = { x | ( x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) /\ S C_ x ) }
19 df-rab 
 |-  { x e. ( SubRing ` W ) | ( ran C u. S ) C_ x } = { x | ( x e. ( SubRing ` W ) /\ ( ran C u. S ) C_ x ) }
20 17 18 19 3eqtr4g 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> { x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ x } = { x e. ( SubRing ` W ) | ( ran C u. S ) C_ x } )
21 20 inteqd 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> |^| { x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ x } = |^| { x e. ( SubRing ` W ) | ( ran C u. S ) C_ x } )
22 1 4 9 aspval 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = |^| { x e. ( ( SubRing ` W ) i^i ( LSubSp ` W ) ) | S C_ x } )
23 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
24 4 subrgmre 
 |-  ( W e. Ring -> ( SubRing ` W ) e. ( Moore ` V ) )
25 23 24 syl 
 |-  ( W e. AssAlg -> ( SubRing ` W ) e. ( Moore ` V ) )
26 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
27 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
28 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
29 2 26 23 27 28 4 asclf 
 |-  ( W e. AssAlg -> C : ( Base ` ( Scalar ` W ) ) --> V )
30 29 frnd 
 |-  ( W e. AssAlg -> ran C C_ V )
31 30 adantr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ran C C_ V )
32 simpr 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> S C_ V )
33 31 32 unssd 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( ran C u. S ) C_ V )
34 3 mrcval 
 |-  ( ( ( SubRing ` W ) e. ( Moore ` V ) /\ ( ran C u. S ) C_ V ) -> ( R ` ( ran C u. S ) ) = |^| { x e. ( SubRing ` W ) | ( ran C u. S ) C_ x } )
35 25 33 34 syl2an2r 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( R ` ( ran C u. S ) ) = |^| { x e. ( SubRing ` W ) | ( ran C u. S ) C_ x } )
36 21 22 35 3eqtr4d 
 |-  ( ( W e. AssAlg /\ S C_ V ) -> ( A ` S ) = ( R ` ( ran C u. S ) ) )