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	$⊢ AlgSpan = (w \in AssAlg ⟼ (s \in 𝒫 {Base}_{w} ⟼ ⋂ \{t \in (SubRing (w) \cap LSubSp (w)) \| s \subseteq t\}))$

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

Metamath Proof Explorer