Metamath Proof Explorer

Definition df-lss

Description: Define the set of linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013)

Ref Expression
Assertion df-lss ⊢LSubSp=w∈V⟼s∈𝒫Basew∖∅|∀x∈BaseScalar⁡w∀a∈s∀b∈sx⋅wa+wb∈s

Detailed syntax breakdown

Step Hyp Ref Expression
0 clss classLSubSp
1 vw setvarw
2 cvv classV
3 vs setvars
4 cbs classBase
5 1 cv setvarw
6 5 4 cfv classBasew
7 6 cpw class𝒫Basew
8 c0 class∅
9 8 csn class∅
10 7 9 cdif class𝒫Basew∖∅
11 vx setvarx
12 csca classScalar
13 5 12 cfv classScalar⁡w
14 13 4 cfv classBaseScalar⁡w
15 va setvara
16 3 cv setvars
17 vb setvarb
18 11 cv setvarx
19 cvsca class⋅𝑠
20 5 19 cfv class⋅w
21 15 cv setvara
22 18 21 20 co classx⋅wa
23 cplusg class+𝑔
24 5 23 cfv class+w
25 17 cv setvarb
26 22 25 24 co classx⋅wa+wb
27 26 16 wcel wffx⋅wa+wb∈s
28 27 17 16 wral wff∀b∈sx⋅wa+wb∈s
29 28 15 16 wral wff∀a∈s∀b∈sx⋅wa+wb∈s
30 29 11 14 wral wff∀x∈BaseScalar⁡w∀a∈s∀b∈sx⋅wa+wb∈s
31 30 3 10 crab classs∈𝒫Basew∖∅|∀x∈BaseScalar⁡w∀a∈s∀b∈sx⋅wa+wb∈s
32 1 2 31 cmpt classw∈V⟼s∈𝒫Basew∖∅|∀x∈BaseScalar⁡w∀a∈s∀b∈sx⋅wa+wb∈s
33 0 32 wceq wffLSubSp=w∈V⟼s∈𝒫Basew∖∅|∀x∈BaseScalar⁡w∀a∈s∀b∈sx⋅wa+wb∈s