Definition df-asp 22162

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

Assertion

Ref	Expression
df-asp	⊢ AlgSpan = (𝑤 ∈ AssAlg ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}))

Distinct variable group:   𝑡,𝑠,𝑤

Detailed syntax breakdown of Definition df-asp

Step	Hyp	Ref	Expression
1		casp 22159	. 2 class AlgSpan
2		vw	. . 3 setvar 𝑤
3		casa 22158	. . 3 class AssAlg
4		vs	. . . 4 setvar 𝑠
5	2	cv 1569	. . . . . 6 class 𝑤
6		cbs 17387	. . . . . 6 class Base
7	5, 6	cfv 6538	. . . . 5 class (Base‘𝑤)
8	7	cpw 4557	. . . 4 class 𝒫 (Base‘𝑤)
9	4	cv 1569	. . . . . . 7 class 𝑠
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1569	. . . . . . 7 class 𝑡
12	9, 11	wss 3899	. . . . . 6 wff 𝑠 ⊆ 𝑡
13		csubrg 20821	. . . . . . . 8 class SubRing
14	5, 13	cfv 6538	. . . . . . 7 class (SubRing‘𝑤)
15		clss 21206	. . . . . . . 8 class LSubSp
16	5, 15	cfv 6538	. . . . . . 7 class (LSubSp‘𝑤)
17	14, 16	cin 3898	. . . . . 6 class ((SubRing‘𝑤) ∩ (LSubSp‘𝑤))
18	12, 10, 17	crab 3413	. . . . 5 class {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}
19	18	cint 4907	. . . 4 class ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}
20	4, 8, 19	cmpt 5186	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})
21	2, 3, 20	cmpt 5186	. 2 class (𝑤 ∈ AssAlg ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}))
22	1, 21	wceq 1570	1 wff AlgSpan = (𝑤 ∈ AssAlg ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}))

This definition is used by:  aspval  22180