Definition df-lssm 13909

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 13908	. 2 class LSubSp
2		vw	. . 3 setvar 𝑤
3		cvv 2763	. . 3 class V
4		vj	. . . . . . 7 setvar 𝑗
5		vs	. . . . . . 7 setvar 𝑠
6	4, 5	wel 2168	. . . . . 6 wff 𝑗 ∈ 𝑠
7	6, 4	wex 1506	. . . . 5 wff ∃𝑗 𝑗 ∈ 𝑠
8		vx	. . . . . . . . . . . 12 setvar 𝑥
9	8	cv 1363	. . . . . . . . . . 11 class 𝑥
10		va	. . . . . . . . . . . 12 setvar 𝑎
11	10	cv 1363	. . . . . . . . . . 11 class 𝑎
12	2	cv 1363	. . . . . . . . . . . 12 class 𝑤
13		cvsca 12759	. . . . . . . . . . . 12 class ·𝑠
14	12, 13	cfv 5258	. . . . . . . . . . 11 class ( ·𝑠 ‘𝑤)
15	9, 11, 14	co 5922	. . . . . . . . . 10 class (𝑥( ·𝑠 ‘𝑤)𝑎)
16		vb	. . . . . . . . . . 11 setvar 𝑏
17	16	cv 1363	. . . . . . . . . 10 class 𝑏
18		cplusg 12755	. . . . . . . . . . 11 class +g
19	12, 18	cfv 5258	. . . . . . . . . 10 class (+g‘𝑤)
20	15, 17, 19	co 5922	. . . . . . . . 9 class ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏)
21	5	cv 1363	. . . . . . . . 9 class 𝑠
22	20, 21	wcel 2167	. . . . . . . 8 wff ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
23	22, 16, 21	wral 2475	. . . . . . 7 wff ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
24	23, 10, 21	wral 2475	. . . . . 6 wff ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
25		csca 12758	. . . . . . . 8 class Scalar
26	12, 25	cfv 5258	. . . . . . 7 class (Scalar‘𝑤)
27		cbs 12678	. . . . . . 7 class Base
28	26, 27	cfv 5258	. . . . . 6 class (Base‘(Scalar‘𝑤))
29	24, 8, 28	wral 2475	. . . . 5 wff ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠
30	7, 29	wa 104	. . . 4 wff (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)
31	12, 27	cfv 5258	. . . . 5 class (Base‘𝑤)
32	31	cpw 3605	. . . 4 class 𝒫 (Base‘𝑤)
33	30, 5, 32	crab 2479	. . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)}
34	2, 3, 33	cmpt 4094	. 2 class (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)})
35	1, 34	wceq 1364	1 wff LSubSp = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (∃𝑗 𝑗 ∈ 𝑠 ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠)})

This definition is referenced by:  lssex  13910  lssmex  13911  lsssetm  13912  lidlmex  14031