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 AssAlg S V A S = R ran C 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 SubRing W LSubSp W x SubRing W x LSubSp W
6 5 anbi1i x SubRing W LSubSp W S x x SubRing W x LSubSp W S x
7 anass x SubRing W x LSubSp W S x x SubRing W x LSubSp W S x
8 6 7 bitri x SubRing W LSubSp W S x x SubRing W x LSubSp W S x
9 eqid LSubSp W = LSubSp W
10 2 9 issubassa2 W AssAlg x SubRing W x LSubSp W ran C x
11 10 anbi1d W AssAlg x SubRing W x LSubSp W S x ran C x S x
12 unss ran C x S x ran C S x
13 11 12 syl6bb W AssAlg x SubRing W x LSubSp W S x ran C S x
14 13 pm5.32da W AssAlg x SubRing W x LSubSp W S x x SubRing W ran C S x
15 8 14 syl5bb W AssAlg x SubRing W LSubSp W S x x SubRing W ran C S x
16 15 abbidv W AssAlg x | x SubRing W LSubSp W S x = x | x SubRing W ran C S x
17 16 adantr W AssAlg S V x | x SubRing W LSubSp W S x = x | x SubRing W ran C S x
18 df-rab x SubRing W LSubSp W | S x = x | x SubRing W LSubSp W S x
19 df-rab x SubRing W | ran C S x = x | x SubRing W ran C S x
20 17 18 19 3eqtr4g W AssAlg S V x SubRing W LSubSp W | S x = x SubRing W | ran C S x
21 20 inteqd W AssAlg S V x SubRing W LSubSp W | S x = x SubRing W | ran C S x
22 1 4 9 aspval W AssAlg S V A S = x SubRing W LSubSp W | S x
23 assaring W AssAlg W Ring
24 4 subrgmre W Ring SubRing W Moore V
25 23 24 syl W AssAlg SubRing W Moore V
26 eqid Scalar W = Scalar W
27 assalmod W AssAlg W LMod
28 eqid Base Scalar W = Base Scalar W
29 2 26 23 27 28 4 asclf W AssAlg C : Base Scalar W V
30 29 frnd W AssAlg ran C V
31 30 adantr W AssAlg S V ran C V
32 simpr W AssAlg S V S V
33 31 32 unssd W AssAlg S V ran C S V
34 3 mrcval SubRing W Moore V ran C S V R ran C S = x SubRing W | ran C S x
35 25 33 34 syl2an2r W AssAlg S V R ran C S = x SubRing W | ran C S x
36 21 22 35 3eqtr4d W AssAlg S V A S = R ran C S