# 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 ${⊢}\mathrm{LSubSp}=\left({w}\in \mathrm{V}⟼\left\{{s}\in \left(𝒫{\mathrm{Base}}_{{w}}\setminus \left\{\varnothing \right\}\right)|\forall {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}\phantom{\rule{.4em}{0ex}}\forall {a}\in {s}\phantom{\rule{.4em}{0ex}}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clss ${class}\mathrm{LSubSp}$
1 vw ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vs ${setvar}{s}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{w}}$
7 6 cpw ${class}𝒫{\mathrm{Base}}_{{w}}$
8 c0 ${class}\varnothing$
9 8 csn ${class}\left\{\varnothing \right\}$
10 7 9 cdif ${class}\left(𝒫{\mathrm{Base}}_{{w}}\setminus \left\{\varnothing \right\}\right)$
11 vx ${setvar}{x}$
12 csca ${class}\mathrm{Scalar}$
13 5 12 cfv ${class}\mathrm{Scalar}\left({w}\right)$
14 13 4 cfv ${class}{\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}$
15 va ${setvar}{a}$
16 3 cv ${setvar}{s}$
17 vb ${setvar}{b}$
18 11 cv ${setvar}{x}$
19 cvsca ${class}{\cdot }_{𝑠}$
20 5 19 cfv ${class}{\cdot }_{{w}}$
21 15 cv ${setvar}{a}$
22 18 21 20 co ${class}\left({x}{\cdot }_{{w}}{a}\right)$
23 cplusg ${class}{+}_{𝑔}$
24 5 23 cfv ${class}{+}_{{w}}$
25 17 cv ${setvar}{b}$
26 22 25 24 co ${class}\left(\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\right)$
27 26 16 wcel ${wff}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}$
28 27 17 16 wral ${wff}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}$
29 28 15 16 wral ${wff}\forall {a}\in {s}\phantom{\rule{.4em}{0ex}}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}$
30 29 11 14 wral ${wff}\forall {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}\phantom{\rule{.4em}{0ex}}\forall {a}\in {s}\phantom{\rule{.4em}{0ex}}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}$
31 30 3 10 crab ${class}\left\{{s}\in \left(𝒫{\mathrm{Base}}_{{w}}\setminus \left\{\varnothing \right\}\right)|\forall {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}\phantom{\rule{.4em}{0ex}}\forall {a}\in {s}\phantom{\rule{.4em}{0ex}}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}\right\}$
32 1 2 31 cmpt ${class}\left({w}\in \mathrm{V}⟼\left\{{s}\in \left(𝒫{\mathrm{Base}}_{{w}}\setminus \left\{\varnothing \right\}\right)|\forall {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}\phantom{\rule{.4em}{0ex}}\forall {a}\in {s}\phantom{\rule{.4em}{0ex}}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}\right\}\right)$
33 0 32 wceq ${wff}\mathrm{LSubSp}=\left({w}\in \mathrm{V}⟼\left\{{s}\in \left(𝒫{\mathrm{Base}}_{{w}}\setminus \left\{\varnothing \right\}\right)|\forall {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}\phantom{\rule{.4em}{0ex}}\forall {a}\in {s}\phantom{\rule{.4em}{0ex}}\forall {b}\in {s}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{w}}{a}\right){+}_{{w}}{b}\in {s}\right\}\right)$