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 25779
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 25778 . 2  class  - cv
2 vn . . 3  set  n
3 cn 9762 . . 3  class  NN
4 vu . . . 4  set  u
5 cc 8751 . . . . 5  class  CC
6 c1 8754 . . . . . 6  class  1
72cv 1631 . . . . . 6  class  n
8 cfz 10798 . . . . . 6  class  ...
96, 7, 8co 5874 . . . . 5  class  ( 1 ... n )
10 cmap 6788 . . . . 5  class  ^m
115, 9, 10co 5874 . . . 4  class  ( CC 
^m  ( 1 ... n ) )
12 c0cv 25753 . . . . . 6  class  0 cv
137, 12cfv 5271 . . . . 5  class  ( 0 cv `  n )
144cv 1631 . . . . 5  class  u
15 cmcv 25767 . . . . . 6  class  - cv
167, 15cfv 5271 . . . . 5  class  (  - cv  `  n )
1713, 14, 16co 5874 . . . 4  class  ( ( 0 cv `  n
) (  - cv  `  n ) u )
184, 11, 17cmpt 4093 . . 3  class  ( u  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( ( 0 cv `  n
) (  - cv  `  n ) u ) )
192, 3, 18cmpt 4093 . 2  class  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( ( 0 cv `  n
) (  - cv  `  n ) u ) ) )
201, 19wceq 1632 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  25780
  Copyright terms: Public domain W3C validator