Definition df-lss 15964

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 15963	. 2 class LSubSp
2		vw	. . 3 set w
3		cvv 2916	. . 3 class _V
4		vx	. . . . . . . . . . 11 set x
5	4	cv 1648	. . . . . . . . . 10 class x
6		va	. . . . . . . . . . 11 set a
7	6	cv 1648	. . . . . . . . . 10 class a
8	2	cv 1648	. . . . . . . . . . 11 class w
9		cvsca 13488	. . . . . . . . . . 11 class .s
10	8, 9	cfv 5413	. . . . . . . . . 10 class ( .s ` w )
11	5, 7, 10	co 6040	. . . . . . . . 9 class ( x ( .s ` w ) a )
12		vb	. . . . . . . . . 10 set b
13	12	cv 1648	. . . . . . . . 9 class b
14		cplusg 13484	. . . . . . . . . 10 class +g
15	8, 14	cfv 5413	. . . . . . . . 9 class ( +g ` w )
16	11, 13, 15	co 6040	. . . . . . . 8 class ( ( x ( .s ` w ) a ) ( +g ` w ) b )
17		vs	. . . . . . . . 9 set s
18	17	cv 1648	. . . . . . . 8 class s
19	16, 18	wcel 1721	. . . . . . 7 wff ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
20	19, 12, 18	wral 2666	. . . . . 6 wff A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
21	20, 6, 18	wral 2666	. . . . 5 wff A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
22		csca 13487	. . . . . . 7 class Scalar
23	8, 22	cfv 5413	. . . . . 6 class (Scalar ` w )
24		cbs 13424	. . . . . 6 class Base
25	23, 24	cfv 5413	. . . . 5 class ( Base ` (Scalar ` w ) )
26	21, 4, 25	wral 2666	. . . 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 5413	. . . . . 6 class ( Base ` w )
28	27	cpw 3759	. . . . 5 class ~P ( Base ` w )
29		c0 3588	. . . . . 6 class (/)
30	29	csn 3774	. . . . 5 class { (/) }
31	28, 30	cdif 3277	. . . 4 class ( ~P ( Base ` w ) \ { (/) } )
32	26, 17, 31	crab 2670	. . 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 4226	. 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 1649	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  15965