Definition df-lss 20109

Description: Define the set of linear subspaces of a left module or left vector space. (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 20108	. 2 class LSubSp
2		vw	. . 3 setvar 𝑤
3		cvv 3422	. . 3 class V
4		vx	. . . . . . . . . . 11 setvar 𝑥
5	4	cv 1538	. . . . . . . . . 10 class 𝑥
6		va	. . . . . . . . . . 11 setvar 𝑎
7	6	cv 1538	. . . . . . . . . 10 class 𝑎
8	2	cv 1538	. . . . . . . . . . 11 class 𝑤
9		cvsca 16892	. . . . . . . . . . 11 class ·𝑠
10	8, 9	cfv 6418	. . . . . . . . . 10 class ( ·𝑠 ‘𝑤)
11	5, 7, 10	co 7255	. . . . . . . . 9 class (𝑥( ·𝑠 ‘𝑤)𝑎)
12		vb	. . . . . . . . . 10 setvar 𝑏
13	12	cv 1538	. . . . . . . . 9 class 𝑏
14		cplusg 16888	. . . . . . . . . 10 class +g
15	8, 14	cfv 6418	. . . . . . . . 9 class (+g‘𝑤)
16	11, 13, 15	co 7255	. . . . . . . 8 class ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏)
17		vs	. . . . . . . . 9 setvar 𝑠
18	17	cv 1538	. . . . . . . 8 class 𝑠
19	16, 18	wcel 2108	. . . . . . 7 wff ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
20	19, 12, 18	wral 3063	. . . . . 6 wff ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
21	20, 6, 18	wral 3063	. . . . 5 wff ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
22		csca 16891	. . . . . . 7 class Scalar
23	8, 22	cfv 6418	. . . . . 6 class (Scalar‘𝑤)
24		cbs 16840	. . . . . 6 class Base
25	23, 24	cfv 6418	. . . . 5 class (Base‘(Scalar‘𝑤))
26	21, 4, 25	wral 3063	. . . 4 wff ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
27	8, 24	cfv 6418	. . . . . 6 class (Base‘𝑤)
28	27	cpw 4530	. . . . 5 class 𝒫 (Base‘𝑤)
29		c0 4253	. . . . . 6 class ∅
30	29	csn 4558	. . . . 5 class {∅}
31	28, 30	cdif 3880	. . . 4 class (𝒫 (Base‘𝑤) ∖ {∅})
32	26, 17, 31	crab 3067	. . 3 class {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠}
33	2, 3, 32	cmpt 5153	. 2 class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})
34	1, 33	wceq 1539	1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫 (Base‘𝑤) ∖ {∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠})

This definition is referenced by:  lssset  20110