# Metamath Proof Explorer

## Definition df-asp

Description: Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Assertion df-asp ${⊢}\mathrm{AlgSpan}=\left({w}\in \mathrm{AssAlg}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)|{s}\subseteq {t}\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 casp ${class}\mathrm{AlgSpan}$
1 vw ${setvar}{w}$
2 casa ${class}\mathrm{AssAlg}$
3 vs ${setvar}{s}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{w}}$
7 6 cpw ${class}𝒫{\mathrm{Base}}_{{w}}$
8 vt ${setvar}{t}$
9 csubrg ${class}\mathrm{SubRing}$
10 5 9 cfv ${class}\mathrm{SubRing}\left({w}\right)$
11 clss ${class}\mathrm{LSubSp}$
12 5 11 cfv ${class}\mathrm{LSubSp}\left({w}\right)$
13 10 12 cin ${class}\left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)$
14 3 cv ${setvar}{s}$
15 8 cv ${setvar}{t}$
16 14 15 wss ${wff}{s}\subseteq {t}$
17 16 8 13 crab ${class}\left\{{t}\in \left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)|{s}\subseteq {t}\right\}$
18 17 cint ${class}\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)|{s}\subseteq {t}\right\}$
19 3 7 18 cmpt ${class}\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)|{s}\subseteq {t}\right\}\right)$
20 1 2 19 cmpt ${class}\left({w}\in \mathrm{AssAlg}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)|{s}\subseteq {t}\right\}\right)\right)$
21 0 20 wceq ${wff}\mathrm{AlgSpan}=\left({w}\in \mathrm{AssAlg}⟼\left({s}\in 𝒫{\mathrm{Base}}_{{w}}⟼\bigcap \left\{{t}\in \left(\mathrm{SubRing}\left({w}\right)\cap \mathrm{LSubSp}\left({w}\right)\right)|{s}\subseteq {t}\right\}\right)\right)$