Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ucv Unicode version

Definition df-ucv 25088
Description: Negative of a complex vector. Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-ucv  |-  - cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) 
|->  ( ( 0 cv
`  n ) (  - cv  `  n
) u ) ) )
Distinct variable group:    u, n

Detailed syntax breakdown of Definition df-ucv
StepHypRef Expression
1 cnegcv 25087 . 2  class  - cv
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 vu . . . 4  set  u
5 cc 8735 . . . . 5  class  CC
6 c1 8738 . . . . . 6  class  1
72cv 1622 . . . . . 6  class  n
8 cfz 10782 . . . . . 6  class  ...
96, 7, 8co 5858 . . . . 5  class  ( 1 ... n )
10 cmap 6772 . . . . 5  class  ^m
115, 9, 10co 5858 . . . 4  class  ( CC 
^m  ( 1 ... n ) )
12 c0cv 25062 . . . . . 6  class  0 cv
137, 12cfv 5255 . . . . 5  class  ( 0 cv `  n )
144cv 1622 . . . . 5  class  u
15 cmcv 25076 . . . . . 6  class  - cv
167, 15cfv 5255 . . . . 5  class  (  - cv  `  n )
1713, 14, 16co 5858 . . . 4  class  ( ( 0 cv `  n
) (  - cv  `  n ) u )
184, 11, 17cmpt 4077 . . 3  class  ( u  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( ( 0 cv `  n
) (  - cv  `  n ) u ) )
192, 3, 18cmpt 4077 . 2  class  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( ( 0 cv `  n
) (  - cv  `  n ) u ) ) )
201, 19wceq 1623 1  wff  - cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) 
|->  ( ( 0 cv
`  n ) (  - cv  `  n
) u ) ) )
Colors of variables: wff set class
This definition is referenced by:  isucv  25089
  Copyright terms: Public domain W3C validator