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 = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s ) } )

Distinct variable group:   a, b, j, s, x, w

Detailed syntax breakdown of Definition df-lssm

Step	Hyp	Ref	Expression
1		clss 13908	. 2 class LSubSp
2		vw	. . 3 setvar w
3		cvv 2763	. . 3 class _V
4		vj	. . . . . . 7 setvar j
5		vs	. . . . . . 7 setvar s
6	4, 5	wel 2168	. . . . . 6 wff j e. s
7	6, 4	wex 1506	. . . . 5 wff E. j j e. s
8		vx	. . . . . . . . . . . 12 setvar x
9	8	cv 1363	. . . . . . . . . . 11 class x
10		va	. . . . . . . . . . . 12 setvar a
11	10	cv 1363	. . . . . . . . . . 11 class a
12	2	cv 1363	. . . . . . . . . . . 12 class w
13		cvsca 12759	. . . . . . . . . . . 12 class .s
14	12, 13	cfv 5258	. . . . . . . . . . 11 class ( .s ` w )
15	9, 11, 14	co 5922	. . . . . . . . . 10 class ( x ( .s ` w ) a )
16		vb	. . . . . . . . . . 11 setvar b
17	16	cv 1363	. . . . . . . . . 10 class b
18		cplusg 12755	. . . . . . . . . . 11 class +g
19	12, 18	cfv 5258	. . . . . . . . . 10 class ( +g ` w )
20	15, 17, 19	co 5922	. . . . . . . . 9 class ( ( x ( .s ` w ) a ) ( +g ` w ) b )
21	5	cv 1363	. . . . . . . . 9 class s
22	20, 21	wcel 2167	. . . . . . . 8 wff ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
23	22, 16, 21	wral 2475	. . . . . . 7 wff A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
24	23, 10, 21	wral 2475	. . . . . 6 wff A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
25		csca 12758	. . . . . . . 8 class Scalar
26	12, 25	cfv 5258	. . . . . . 7 class (Scalar ` w )
27		cbs 12678	. . . . . . 7 class Base
28	26, 27	cfv 5258	. . . . . 6 class ( Base ` (Scalar ` w ) )
29	24, 8, 28	wral 2475	. . . . 5 wff A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
30	7, 29	wa 104	. . . 4 wff ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s )
31	12, 27	cfv 5258	. . . . 5 class ( Base ` w )
32	31	cpw 3605	. . . 4 class ~P ( Base ` w )
33	30, 5, 32	crab 2479	. . 3 class { s e. ~P ( Base ` w ) | ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s ) }
34	2, 3, 33	cmpt 4094	. 2 class ( w e. _V |-> { s e. ~P ( Base ` w ) | ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s ) } )
35	1, 34	wceq 1364	1 wff LSubSp = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s ) } )

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