Definition df-lssm 14366

Description: A linear subspace of a left module or left vector space is an inhabited (in contrast to non-empty for non-intuitionistic logic) 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-lssm	⊢ LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)})

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

Detailed syntax breakdown of Definition df-lssm

Step	Hyp	Ref	Expression
1		clss 14365	. 2 class LSubSp
2		vw	. . 3 setvar 𝑤
3		cvv 2802	. . 3 class V
4		vj	. . . . . . 7 setvar 𝑗
5		vs	. . . . . . 7 setvar 𝑠
6	4, 5	wel 2203	. . . . . 6 wff 𝑗 ∈ 𝑠
7	6, 4	wex 1540	. . . . 5 wff ∃𝑗 𝑗 ∈ 𝑠
8		vx	. . . . . . . . . . . 12 setvar 𝑥
9	8	cv 1396	. . . . . . . . . . 11 class 𝑥
10		va	. . . . . . . . . . . 12 setvar 𝑎
11	10	cv 1396	. . . . . . . . . . 11 class 𝑎
12	2	cv 1396	. . . . . . . . . . . 12 class 𝑤
13		cvsca 13163	. . . . . . . . . . . 12 class ·𝑠
14	12, 13	cfv 5326	. . . . . . . . . . 11 class ( ·𝑠 ‘𝑤)
15	9, 11, 14	co 6017	. . . . . . . . . 10 class (𝑥( ·𝑠 ‘𝑤)𝑎)
16		vb	. . . . . . . . . . 11 setvar 𝑏
17	16	cv 1396	. . . . . . . . . 10 class 𝑏
18		cplusg 13159	. . . . . . . . . . 11 class +g
19	12, 18	cfv 5326	. . . . . . . . . 10 class (+g‘𝑤)
20	15, 17, 19	co 6017	. . . . . . . . 9 class ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏)
21	5	cv 1396	. . . . . . . . 9 class 𝑠
22	20, 21	wcel 2202	. . . . . . . 8 wff ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
23	22, 16, 21	wral 2510	. . . . . . 7 wff ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
24	23, 10, 21	wral 2510	. . . . . 6 wff ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
25		csca 13162	. . . . . . . 8 class Scalar
26	12, 25	cfv 5326	. . . . . . 7 class (Scalar‘𝑤)
27		cbs 13081	. . . . . . 7 class Base
28	26, 27	cfv 5326	. . . . . 6 class (Base‘(Scalar‘𝑤))
29	24, 8, 28	wral 2510	. . . . 5 wff ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
30	7, 29	wa 104	. . . 4 wff (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)
31	12, 27	cfv 5326	. . . . 5 class (Base‘𝑤)
32	31	cpw 3652	. . . 4 class 𝒫 (Base‘𝑤)
33	30, 5, 32	crab 2514	. . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)}
34	2, 3, 33	cmpt 4150	. 2 class (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)})
35	1, 34	wceq 1397	1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)})

This definition is referenced by:  lssex  14367  lssmex  14368  lsssetm  14369  lidlmex  14488