Definition df-asp 19134

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 19131	. 2 class AlgSpan
2		vw	. . 3 setvar 𝑤
3		casa 19130	. . 3 class AssAlg
4		vs	. . . 4 setvar 𝑠
5	2	cv 1474	. . . . . 6 class 𝑤
6		cbs 15695	. . . . . 6 class Base
7	5, 6	cfv 5804	. . . . 5 class (Base‘𝑤)
8	7	cpw 4108	. . . 4 class 𝒫 (Base‘𝑤)
9	4	cv 1474	. . . . . . 7 class 𝑠
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1474	. . . . . . 7 class 𝑡
12	9, 11	wss 3540	. . . . . 6 wff 𝑠 ⊆ 𝑡
13		csubrg 18599	. . . . . . . 8 class SubRing
14	5, 13	cfv 5804	. . . . . . 7 class (SubRing‘𝑤)
15		clss 18753	. . . . . . . 8 class LSubSp
16	5, 15	cfv 5804	. . . . . . 7 class (LSubSp‘𝑤)
17	14, 16	cin 3539	. . . . . 6 class ((SubRing‘𝑤) ∩ (LSubSp‘𝑤))
18	12, 10, 17	crab 2900	. . . . 5 class {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}
19	18	cint 4410	. . . 4 class ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}
20	4, 8, 19	cmpt 4643	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})
21	2, 3, 20	cmpt 4643	. 2 class (𝑤 ∈ AssAlg ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}))
22	1, 21	wceq 1475	1 wff AlgSpan = (𝑤 ∈ AssAlg ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡}))

This definition is referenced by:  aspval  19149