Definition df-ssp 27577

Description: Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-ssp	|- SubSp = ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )

Distinct variable group:   w, u

Detailed syntax breakdown of Definition df-ssp

Step	Hyp	Ref	Expression
1		css 27576	. 2 class SubSp
2		vu	. . 3 setvar u
3		cnv 27439	. . 3 class NrmCVec
4		vw	. . . . . . . 8 setvar w
5	4	cv 1482	. . . . . . 7 class w
6		cpv 27440	. . . . . . 7 class +v
7	5, 6	cfv 5888	. . . . . 6 class ( +v ` w )
8	2	cv 1482	. . . . . . 7 class u
9	8, 6	cfv 5888	. . . . . 6 class ( +v ` u )
10	7, 9	wss 3574	. . . . 5 wff ( +v ` w ) C_ ( +v ` u )
11		cns 27442	. . . . . . 7 class .sOLD
12	5, 11	cfv 5888	. . . . . 6 class ( .sOLD ` w )
13	8, 11	cfv 5888	. . . . . 6 class ( .sOLD ` u )
14	12, 13	wss 3574	. . . . 5 wff ( .sOLD ` w ) C_ ( .sOLD ` u )
15		cnmcv 27445	. . . . . . 7 class normCV
16	5, 15	cfv 5888	. . . . . 6 class ( normCV ` w )
17	8, 15	cfv 5888	. . . . . 6 class ( normCV ` u )
18	16, 17	wss 3574	. . . . 5 wff ( normCV ` w ) C_ ( normCV ` u )
19	10, 14, 18	w3a 1037	. . . 4 wff ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) )
20	19, 4, 3	crab 2916	. . 3 class { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) }
21	2, 3, 20	cmpt 4729	. 2 class ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )
22	1, 21	wceq 1483	1 wff SubSp = ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )

This definition is referenced by:  sspval  27578