Metamath Proof Explorer

Definition df-ssp

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 css 
 |-  SubSp
1 vu 
 |-  u
2 cnv 
 |-  NrmCVec
3 vw 
 |-  w
4 cpv 
 |-  +v
5 3 cv 
 |-  w
6 5 4 cfv 
 |-  ( +v ` w )
7 1 cv 
 |-  u
8 7 4 cfv 
 |-  ( +v ` u )
9 6 8 wss 
 |-  ( +v ` w ) C_ ( +v ` u )
10 cns 
 |-  .sOLD
11 5 10 cfv 
 |-  ( .sOLD ` w )
12 7 10 cfv 
 |-  ( .sOLD ` u )
13 11 12 wss 
 |-  ( .sOLD ` w ) C_ ( .sOLD ` u )
14 cnmcv 
 |-  normCV
15 5 14 cfv 
 |-  ( normCV ` w )
16 7 14 cfv 
 |-  ( normCV ` u )
17 15 16 wss 
 |-  ( normCV ` w ) C_ ( normCV ` u )
18 9 13 17 w3a 
 |-  ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) )
19 18 3 2 crab 
 |-  { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) }
20 1 2 19 cmpt 
 |-  ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )
21 0 20 wceq 
 |-  SubSp = ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } )