Definition df-lss 21207

Description: Define the set of linear subspaces of a left module or left vector space: a linear subspace of a left module or left vector space is a non-empty subset of the base set of the left module/vector space with a closure condition on vector addition and scalar multiplication. (Contributed by NM, 8-Dec-2013.)

Assertion

Ref	Expression
df-lss	⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})

Distinct variable group:   𝑎,𝑏,𝑠,𝑥,𝑤

Detailed syntax breakdown of Definition df-lss

Step	Hyp	Ref	Expression
1		clss 21206	. 2 class LSubSp
2		vw	. . 3 setvar 𝑤
3		cvv 3450	. . 3 class V
4		vx	. . . . . . . . . . 11 setvar 𝑥
5	4	cv 1568	. . . . . . . . . 10 class 𝑥
6		va	. . . . . . . . . . 11 setvar 𝑎
7	6	cv 1568	. . . . . . . . . 10 class 𝑎
8	2	cv 1568	. . . . . . . . . . 11 class 𝑤
9		cvsca 17432	. . . . . . . . . . 11 class ·𝑠
10	8, 9	cfv 6538	. . . . . . . . . 10 class ( ·𝑠 ‘𝑤)
11	5, 7, 10	co 7420	. . . . . . . . 9 class (𝑥( ·𝑠 ‘𝑤)𝑎)
12		vb	. . . . . . . . . 10 setvar 𝑏
13	12	cv 1568	. . . . . . . . 9 class 𝑏
14		cplusg 17428	. . . . . . . . . 10 class +g
15	8, 14	cfv 6538	. . . . . . . . 9 class (+g‘𝑤)
16	11, 13, 15	co 7420	. . . . . . . 8 class ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏)
17		vs	. . . . . . . . 9 setvar 𝑠
18	17	cv 1568	. . . . . . . 8 class 𝑠
19	16, 18	wcel 2144	. . . . . . 7 wff ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
20	19, 12, 18	wral 3076	. . . . . 6 wff ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
21	20, 6, 18	wral 3076	. . . . 5 wff ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
22		csca 17431	. . . . . . 7 class Scalar
23	8, 22	cfv 6538	. . . . . 6 class (Scalar‘𝑤)
24		cbs 17387	. . . . . 6 class Base
25	23, 24	cfv 6538	. . . . 5 class (Base‘(Scalar‘𝑤))
26	21, 4, 25	wral 3076	. . . 4 wff ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
27	8, 24	cfv 6538	. . . . . 6 class (Base‘𝑤)
28	27	cpw 4556	. . . . 5 class 𝒫 (Base‘𝑤)
29		c0 4278	. . . . . 6 class ∅
30	29	csn 4583	. . . . 5 class {∅}
31	28, 30	cdif 4045	. . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
32	26, 17, 31	crab 3412	. . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠}
33	2, 3, 32	cmpt 5185	. 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})
34	1, 33	wceq 1569	1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})

This definition is used by:  lssset  21208