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

Definition df-addcv 25748
Description: Addition of complex vectors in a space of dimension  n. Experimental. (Contributed by FL, 14-Sep-2013.)
Assertion
Ref Expression
df-addcv  |-  + cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) ,  v  e.  ( CC  ^m  ( 1 ... n ) ) 
|->  ( x  e.  ( 1 ... n ) 
|->  ( ( u `  x )  +  ( v `  x ) ) ) ) )
Distinct variable group:    u, n, v, x

Detailed syntax breakdown of Definition df-addcv
StepHypRef Expression
1 cplcv 25747 . 2  class  + cv
2 vn . . 3  set  n
3 cn 9762 . . 3  class  NN
4 vu . . . 4  set  u
5 vv . . . 4  set  v
6 cc 8751 . . . . 5  class  CC
7 c1 8754 . . . . . 6  class  1
82cv 1631 . . . . . 6  class  n
9 cfz 10798 . . . . . 6  class  ...
107, 8, 9co 5874 . . . . 5  class  ( 1 ... n )
11 cmap 6788 . . . . 5  class  ^m
126, 10, 11co 5874 . . . 4  class  ( CC 
^m  ( 1 ... n ) )
13 vx . . . . 5  set  x
1413cv 1631 . . . . . . 7  class  x
154cv 1631 . . . . . . 7  class  u
1614, 15cfv 5271 . . . . . 6  class  ( u `
 x )
175cv 1631 . . . . . . 7  class  v
1814, 17cfv 5271 . . . . . 6  class  ( v `
 x )
19 caddc 8756 . . . . . 6  class  +
2016, 18, 19co 5874 . . . . 5  class  ( ( u `  x )  +  ( v `  x ) )
2113, 10, 20cmpt 4093 . . . 4  class  ( x  e.  ( 1 ... n )  |->  ( ( u `  x )  +  ( v `  x ) ) )
224, 5, 12, 12, 21cmpt2 5876 . . 3  class  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  v  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( x  e.  ( 1 ... n )  |->  ( ( u `  x )  +  ( v `  x ) ) ) )
232, 3, 22cmpt 4093 . 2  class  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  v  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( x  e.  ( 1 ... n )  |->  ( ( u `  x )  +  ( v `  x ) ) ) ) )
241, 23wceq 1632 1  wff  + cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) ,  v  e.  ( CC  ^m  ( 1 ... n ) ) 
|->  ( x  e.  ( 1 ... n ) 
|->  ( ( u `  x )  +  ( v `  x ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  isaddrv  25749  sigadd  25752
  Copyright terms: Public domain W3C validator