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 syl5bb
 |-  ( 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 ) ) )