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

Definition df-nv 21164
Description: Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-nv  |-  NrmCVec  =  { <. <. g ,  s
>. ,  n >.  |  ( <. g ,  s
>.  e.  CVec OLD  /\  n : ran  g --> RR  /\  A. x  e.  ran  g
( ( ( n `
 x )  =  0  ->  x  =  (GId `  g ) )  /\  A. y  e.  CC  ( n `  ( y s x ) )  =  ( ( abs `  y
)  x.  ( n `
 x ) )  /\  A. y  e. 
ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) ) ) ) }
Distinct variable group:    g, s, n, x, y

Detailed syntax breakdown of Definition df-nv
StepHypRef Expression
1 cnv 21156 . 2  class  NrmCVec
2 vg . . . . . . 7  set  g
32cv 1631 . . . . . 6  class  g
4 vs . . . . . . 7  set  s
54cv 1631 . . . . . 6  class  s
63, 5cop 3656 . . . . 5  class  <. g ,  s >.
7 cvc 21117 . . . . 5  class  CVec OLD
86, 7wcel 1696 . . . 4  wff  <. g ,  s >.  e.  CVec OLD
93crn 4706 . . . . 5  class  ran  g
10 cr 8752 . . . . 5  class  RR
11 vn . . . . . 6  set  n
1211cv 1631 . . . . 5  class  n
139, 10, 12wf 5267 . . . 4  wff  n : ran  g --> RR
14 vx . . . . . . . . . 10  set  x
1514cv 1631 . . . . . . . . 9  class  x
1615, 12cfv 5271 . . . . . . . 8  class  ( n `
 x )
17 cc0 8753 . . . . . . . 8  class  0
1816, 17wceq 1632 . . . . . . 7  wff  ( n `
 x )  =  0
19 cgi 20870 . . . . . . . . 9  class GId
203, 19cfv 5271 . . . . . . . 8  class  (GId `  g )
2115, 20wceq 1632 . . . . . . 7  wff  x  =  (GId `  g )
2218, 21wi 4 . . . . . 6  wff  ( ( n `  x )  =  0  ->  x  =  (GId `  g )
)
23 vy . . . . . . . . . . 11  set  y
2423cv 1631 . . . . . . . . . 10  class  y
2524, 15, 5co 5874 . . . . . . . . 9  class  ( y s x )
2625, 12cfv 5271 . . . . . . . 8  class  ( n `
 ( y s x ) )
27 cabs 11735 . . . . . . . . . 10  class  abs
2824, 27cfv 5271 . . . . . . . . 9  class  ( abs `  y )
29 cmul 8758 . . . . . . . . 9  class  x.
3028, 16, 29co 5874 . . . . . . . 8  class  ( ( abs `  y )  x.  ( n `  x ) )
3126, 30wceq 1632 . . . . . . 7  wff  ( n `
 ( y s x ) )  =  ( ( abs `  y
)  x.  ( n `
 x ) )
32 cc 8751 . . . . . . 7  class  CC
3331, 23, 32wral 2556 . . . . . 6  wff  A. y  e.  CC  ( n `  ( y s x ) )  =  ( ( abs `  y
)  x.  ( n `
 x ) )
3415, 24, 3co 5874 . . . . . . . . 9  class  ( x g y )
3534, 12cfv 5271 . . . . . . . 8  class  ( n `
 ( x g y ) )
3624, 12cfv 5271 . . . . . . . . 9  class  ( n `
 y )
37 caddc 8756 . . . . . . . . 9  class  +
3816, 36, 37co 5874 . . . . . . . 8  class  ( ( n `  x )  +  ( n `  y ) )
39 cle 8884 . . . . . . . 8  class  <_
4035, 38, 39wbr 4039 . . . . . . 7  wff  ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) )
4140, 23, 9wral 2556 . . . . . 6  wff  A. y  e.  ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) )
4222, 33, 41w3a 934 . . . . 5  wff  ( ( ( n `  x
)  =  0  ->  x  =  (GId `  g
) )  /\  A. y  e.  CC  (
n `  ( y
s x ) )  =  ( ( abs `  y )  x.  (
n `  x )
)  /\  A. y  e.  ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) ) )
4342, 14, 9wral 2556 . . . 4  wff  A. x  e.  ran  g ( ( ( n `  x
)  =  0  ->  x  =  (GId `  g
) )  /\  A. y  e.  CC  (
n `  ( y
s x ) )  =  ( ( abs `  y )  x.  (
n `  x )
)  /\  A. y  e.  ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) ) )
448, 13, 43w3a 934 . . 3  wff  ( <.
g ,  s >.  e.  CVec OLD  /\  n : ran  g --> RR  /\  A. x  e.  ran  g
( ( ( n `
 x )  =  0  ->  x  =  (GId `  g ) )  /\  A. y  e.  CC  ( n `  ( y s x ) )  =  ( ( abs `  y
)  x.  ( n `
 x ) )  /\  A. y  e. 
ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) ) ) )
4544, 2, 4, 11coprab 5875 . 2  class  { <. <.
g ,  s >. ,  n >.  |  ( <. g ,  s >.  e.  CVec OLD  /\  n : ran  g --> RR  /\  A. x  e.  ran  g
( ( ( n `
 x )  =  0  ->  x  =  (GId `  g ) )  /\  A. y  e.  CC  ( n `  ( y s x ) )  =  ( ( abs `  y
)  x.  ( n `
 x ) )  /\  A. y  e. 
ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) ) ) ) }
461, 45wceq 1632 1  wff  NrmCVec  =  { <. <. g ,  s
>. ,  n >.  |  ( <. g ,  s
>.  e.  CVec OLD  /\  n : ran  g --> RR  /\  A. x  e.  ran  g
( ( ( n `
 x )  =  0  ->  x  =  (GId `  g ) )  /\  A. y  e.  CC  ( n `  ( y s x ) )  =  ( ( abs `  y
)  x.  ( n `
 x ) )  /\  A. y  e. 
ran  g ( n `
 ( x g y ) )  <_ 
( ( n `  x )  +  ( n `  y ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  nvss  21165  isnvlem  21182
  Copyright terms: Public domain W3C validator