Definition df-lss 18933

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

Assertion

Ref	Expression
df-lss	|- LSubSp = ( w e. _V |-> { s e. ( ~P ( Base ` w ) \ { (/) } ) | 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, s, x, w

Detailed syntax breakdown of Definition df-lss

Step	Hyp	Ref	Expression
1		clss 18932	. 2 class LSubSp
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vx	. . . . . . . . . . 11 setvar x
5	4	cv 1482	. . . . . . . . . 10 class x
6		va	. . . . . . . . . . 11 setvar a
7	6	cv 1482	. . . . . . . . . 10 class a
8	2	cv 1482	. . . . . . . . . . 11 class w
9		cvsca 15945	. . . . . . . . . . 11 class .s
10	8, 9	cfv 5888	. . . . . . . . . 10 class ( .s ` w )
11	5, 7, 10	co 6650	. . . . . . . . 9 class ( x ( .s ` w ) a )
12		vb	. . . . . . . . . 10 setvar b
13	12	cv 1482	. . . . . . . . 9 class b
14		cplusg 15941	. . . . . . . . . 10 class +g
15	8, 14	cfv 5888	. . . . . . . . 9 class ( +g ` w )
16	11, 13, 15	co 6650	. . . . . . . 8 class ( ( x ( .s ` w ) a ) ( +g ` w ) b )
17		vs	. . . . . . . . 9 setvar s
18	17	cv 1482	. . . . . . . 8 class s
19	16, 18	wcel 1990	. . . . . . 7 wff ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
20	19, 12, 18	wral 2912	. . . . . 6 wff A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
21	20, 6, 18	wral 2912	. . . . 5 wff A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
22		csca 15944	. . . . . . 7 class Scalar
23	8, 22	cfv 5888	. . . . . 6 class (Scalar ` w )
24		cbs 15857	. . . . . 6 class Base
25	23, 24	cfv 5888	. . . . 5 class ( Base ` (Scalar ` w ) )
26	21, 4, 25	wral 2912	. . . 4 wff A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
27	8, 24	cfv 5888	. . . . . 6 class ( Base ` w )
28	27	cpw 4158	. . . . 5 class ~P ( Base ` w )
29		c0 3915	. . . . . 6 class (/)
30	29	csn 4177	. . . . 5 class { (/) }
31	28, 30	cdif 3571	. . . 4 class ( ~P ( Base ` w ) \ { (/) } )
32	26, 17, 31	crab 2916	. . 3 class { s e. ( ~P ( Base ` w ) \ { (/) } ) | A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s }
33	2, 3, 32	cmpt 4729	. 2 class ( w e. _V |-> { s e. ( ~P ( Base ` w ) \ { (/) } ) | A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s } )
34	1, 33	wceq 1483	1 wff LSubSp = ( w e. _V |-> { s e. ( ~P ( Base ` w ) \ { (/) } ) | 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:  lssset  18934