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

Definition df-0o 21325
Description: Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-0o  |-  0op  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  ( ( BaseSet `  u )  X.  {
( 0vec `  w ) } ) )
Distinct variable group:    w, u

Detailed syntax breakdown of Definition df-0o
StepHypRef Expression
1 c0o 21321 . 2  class  0op
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21140 . . 3  class  NrmCVec
52cv 1622 . . . . 5  class  u
6 cba 21142 . . . . 5  class  BaseSet
75, 6cfv 5255 . . . 4  class  ( BaseSet `  u )
83cv 1622 . . . . . 6  class  w
9 cn0v 21144 . . . . . 6  class  0vec
108, 9cfv 5255 . . . . 5  class  ( 0vec `  w )
1110csn 3640 . . . 4  class  { (
0vec `  w ) }
127, 11cxp 4687 . . 3  class  ( (
BaseSet `  u )  X. 
{ ( 0vec `  w
) } )
132, 3, 4, 4, 12cmpt2 5860 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  ( ( BaseSet `  u
)  X.  { (
0vec `  w ) } ) )
141, 13wceq 1623 1  wff  0op  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  ( ( BaseSet `  u )  X.  {
( 0vec `  w ) } ) )
Colors of variables: wff set class
This definition is referenced by:  0ofval  21365
  Copyright terms: Public domain W3C validator