# 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}=\mathrm{AlgSpan}\left({W}\right)$
aspval2.c ${⊢}{C}=\mathrm{algSc}\left({W}\right)$
aspval2.r ${⊢}{R}=\mathrm{mrCls}\left(\mathrm{SubRing}\left({W}\right)\right)$
aspval2.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
Assertion aspval2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {A}\left({S}\right)={R}\left(\mathrm{ran}{C}\cup {S}\right)$

### Proof

Step Hyp Ref Expression
1 aspval2.a ${⊢}{A}=\mathrm{AlgSpan}\left({W}\right)$
2 aspval2.c ${⊢}{C}=\mathrm{algSc}\left({W}\right)$
3 aspval2.r ${⊢}{R}=\mathrm{mrCls}\left(\mathrm{SubRing}\left({W}\right)\right)$
4 aspval2.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
5 elin ${⊢}{x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)↔\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge {x}\in \mathrm{LSubSp}\left({W}\right)\right)$
6 5 anbi1i ${⊢}\left({x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)↔\left(\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge {x}\in \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)$
7 anass ${⊢}\left(\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge {x}\in \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)↔\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \left({x}\in \mathrm{LSubSp}\left({W}\right)\wedge {S}\subseteq {x}\right)\right)$
8 6 7 bitri ${⊢}\left({x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)↔\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \left({x}\in \mathrm{LSubSp}\left({W}\right)\wedge {S}\subseteq {x}\right)\right)$
9 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
10 2 9 issubassa2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {x}\in \mathrm{SubRing}\left({W}\right)\right)\to \left({x}\in \mathrm{LSubSp}\left({W}\right)↔\mathrm{ran}{C}\subseteq {x}\right)$
11 10 anbi1d ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {x}\in \mathrm{SubRing}\left({W}\right)\right)\to \left(\left({x}\in \mathrm{LSubSp}\left({W}\right)\wedge {S}\subseteq {x}\right)↔\left(\mathrm{ran}{C}\subseteq {x}\wedge {S}\subseteq {x}\right)\right)$
12 unss ${⊢}\left(\mathrm{ran}{C}\subseteq {x}\wedge {S}\subseteq {x}\right)↔\mathrm{ran}{C}\cup {S}\subseteq {x}$
13 11 12 syl6bb ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {x}\in \mathrm{SubRing}\left({W}\right)\right)\to \left(\left({x}\in \mathrm{LSubSp}\left({W}\right)\wedge {S}\subseteq {x}\right)↔\mathrm{ran}{C}\cup {S}\subseteq {x}\right)$
14 13 pm5.32da ${⊢}{W}\in \mathrm{AssAlg}\to \left(\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \left({x}\in \mathrm{LSubSp}\left({W}\right)\wedge {S}\subseteq {x}\right)\right)↔\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \mathrm{ran}{C}\cup {S}\subseteq {x}\right)\right)$
15 8 14 syl5bb ${⊢}{W}\in \mathrm{AssAlg}\to \left(\left({x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)↔\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \mathrm{ran}{C}\cup {S}\subseteq {x}\right)\right)$
16 15 abbidv ${⊢}{W}\in \mathrm{AssAlg}\to \left\{{x}|\left({x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)\right\}=\left\{{x}|\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \mathrm{ran}{C}\cup {S}\subseteq {x}\right)\right\}$
17 16 adantr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \left\{{x}|\left({x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)\right\}=\left\{{x}|\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \mathrm{ran}{C}\cup {S}\subseteq {x}\right)\right\}$
18 df-rab ${⊢}\left\{{x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {x}\right\}=\left\{{x}|\left({x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)\wedge {S}\subseteq {x}\right)\right\}$
19 df-rab ${⊢}\left\{{x}\in \mathrm{SubRing}\left({W}\right)|\mathrm{ran}{C}\cup {S}\subseteq {x}\right\}=\left\{{x}|\left({x}\in \mathrm{SubRing}\left({W}\right)\wedge \mathrm{ran}{C}\cup {S}\subseteq {x}\right)\right\}$
20 17 18 19 3eqtr4g ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \left\{{x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {x}\right\}=\left\{{x}\in \mathrm{SubRing}\left({W}\right)|\mathrm{ran}{C}\cup {S}\subseteq {x}\right\}$
21 20 inteqd ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \bigcap \left\{{x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {x}\right\}=\bigcap \left\{{x}\in \mathrm{SubRing}\left({W}\right)|\mathrm{ran}{C}\cup {S}\subseteq {x}\right\}$
22 1 4 9 aspval ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {A}\left({S}\right)=\bigcap \left\{{x}\in \left(\mathrm{SubRing}\left({W}\right)\cap \mathrm{LSubSp}\left({W}\right)\right)|{S}\subseteq {x}\right\}$
23 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
24 4 subrgmre ${⊢}{W}\in \mathrm{Ring}\to \mathrm{SubRing}\left({W}\right)\in \mathrm{Moore}\left({V}\right)$
25 23 24 syl ${⊢}{W}\in \mathrm{AssAlg}\to \mathrm{SubRing}\left({W}\right)\in \mathrm{Moore}\left({V}\right)$
26 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
27 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
28 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
29 2 26 23 27 28 4 asclf ${⊢}{W}\in \mathrm{AssAlg}\to {C}:{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}⟶{V}$
30 29 frnd ${⊢}{W}\in \mathrm{AssAlg}\to \mathrm{ran}{C}\subseteq {V}$
31 30 adantr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \mathrm{ran}{C}\subseteq {V}$
32 simpr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {S}\subseteq {V}$
33 31 32 unssd ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to \mathrm{ran}{C}\cup {S}\subseteq {V}$
34 3 mrcval ${⊢}\left(\mathrm{SubRing}\left({W}\right)\in \mathrm{Moore}\left({V}\right)\wedge \mathrm{ran}{C}\cup {S}\subseteq {V}\right)\to {R}\left(\mathrm{ran}{C}\cup {S}\right)=\bigcap \left\{{x}\in \mathrm{SubRing}\left({W}\right)|\mathrm{ran}{C}\cup {S}\subseteq {x}\right\}$
35 25 33 34 syl2an2r ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {R}\left(\mathrm{ran}{C}\cup {S}\right)=\bigcap \left\{{x}\in \mathrm{SubRing}\left({W}\right)|\mathrm{ran}{C}\cup {S}\subseteq {x}\right\}$
36 21 22 35 3eqtr4d ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\subseteq {V}\right)\to {A}\left({S}\right)={R}\left(\mathrm{ran}{C}\cup {S}\right)$