MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ssp Unicode version

Definition df-ssp 21300
Description: Define the class of all subspaces of complex normed 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 )  /\  ( .s OLD `  w ) 
C_  ( .s OLD `  u )  /\  ( normCV `  w )  C_  ( normCV `  u ) ) } )
Distinct variable group:    w, u

Detailed syntax breakdown of Definition df-ssp
StepHypRef Expression
1 css 21299 . 2  class  SubSp
2 vu . . 3  set  u
3 cnv 21142 . . 3  class  NrmCVec
4 vw . . . . . . . 8  set  w
54cv 1624 . . . . . . 7  class  w
6 cpv 21143 . . . . . . 7  class  +v
75, 6cfv 5257 . . . . . 6  class  ( +v
`  w )
82cv 1624 . . . . . . 7  class  u
98, 6cfv 5257 . . . . . 6  class  ( +v
`  u )
107, 9wss 3154 . . . . 5  wff  ( +v
`  w )  C_  ( +v `  u )
11 cns 21145 . . . . . . 7  class  .s OLD
125, 11cfv 5257 . . . . . 6  class  ( .s
OLD `  w )
138, 11cfv 5257 . . . . . 6  class  ( .s
OLD `  u )
1412, 13wss 3154 . . . . 5  wff  ( .s
OLD `  w )  C_  ( .s OLD `  u
)
15 cnmcv 21148 . . . . . . 7  class  normCV
165, 15cfv 5257 . . . . . 6  class  ( normCV `  w )
178, 15cfv 5257 . . . . . 6  class  ( normCV `  u )
1816, 17wss 3154 . . . . 5  wff  ( normCV `  w )  C_  ( normCV `  u )
1910, 14, 18w3a 934 . . . 4  wff  ( ( +v `  w ) 
C_  ( +v `  u )  /\  ( .s OLD `  w ) 
C_  ( .s OLD `  u )  /\  ( normCV `  w )  C_  ( normCV `  u ) )
2019, 4, 3crab 2549 . . 3  class  { w  e.  NrmCVec  |  ( ( +v `  w ) 
C_  ( +v `  u )  /\  ( .s OLD `  w ) 
C_  ( .s OLD `  u )  /\  ( normCV `  w )  C_  ( normCV `  u ) ) }
212, 3, 20cmpt 4079 . 2  class  ( u  e.  NrmCVec  |->  { w  e.  NrmCVec  |  ( ( +v
`  w )  C_  ( +v `  u )  /\  ( .s OLD `  w )  C_  ( .s OLD `  u )  /\  ( normCV `  w
)  C_  ( normCV `  u
) ) } )
221, 21wceq 1625 1  wff  SubSp  =  ( u  e.  NrmCVec  |->  { w  e.  NrmCVec  |  ( ( +v `  w ) 
C_  ( +v `  u )  /\  ( .s OLD `  w ) 
C_  ( .s OLD `  u )  /\  ( normCV `  w )  C_  ( normCV `  u ) ) } )
Colors of variables: wff set class
This definition is referenced by:  sspval  21301
  Copyright terms: Public domain W3C validator