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

Definition df-subcatv 25665
Description: Substraction of complex vectors in a space of dimension  n. Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-subcatv  |-  - cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) ,  v  e.  ( CC  ^m  ( 1 ... n ) ) 
|->  ( iota_ w  e.  ( CC  ^m  ( 1 ... n ) ) ( v (  + cv `  n ) w )  =  u ) ) )
Distinct variable group:    u, n, v, w

Detailed syntax breakdown of Definition df-subcatv
StepHypRef Expression
1 cmcv 25664 . 2  class  - cv
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 vu . . . 4  set  u
5 vv . . . 4  set  v
6 cc 8735 . . . . 5  class  CC
7 c1 8738 . . . . . 6  class  1
82cv 1622 . . . . . 6  class  n
9 cfz 10782 . . . . . 6  class  ...
107, 8, 9co 5858 . . . . 5  class  ( 1 ... n )
11 cmap 6772 . . . . 5  class  ^m
126, 10, 11co 5858 . . . 4  class  ( CC 
^m  ( 1 ... n ) )
135cv 1622 . . . . . . 7  class  v
14 vw . . . . . . . 8  set  w
1514cv 1622 . . . . . . 7  class  w
16 cplcv 25644 . . . . . . . 8  class  + cv
178, 16cfv 5255 . . . . . . 7  class  (  + cv `  n )
1813, 15, 17co 5858 . . . . . 6  class  ( v (  + cv `  n
) w )
194cv 1622 . . . . . 6  class  u
2018, 19wceq 1623 . . . . 5  wff  ( v (  + cv `  n
) w )  =  u
2120, 14, 12crio 6297 . . . 4  class  ( iota_ w  e.  ( CC  ^m  ( 1 ... n
) ) ( v (  + cv `  n
) w )  =  u )
224, 5, 12, 12, 21cmpt2 5860 . . 3  class  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  v  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( iota_ w  e.  ( CC  ^m  ( 1 ... n
) ) ( v (  + cv `  n
) w )  =  u ) )
232, 3, 22cmpt 4077 . 2  class  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  v  e.  ( CC  ^m  ( 1 ... n
) )  |->  ( iota_ w  e.  ( CC  ^m  ( 1 ... n
) ) ( v (  + cv `  n
) w )  =  u ) ) )
241, 23wceq 1623 1  wff  - cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) ,  v  e.  ( CC  ^m  ( 1 ... n ) ) 
|->  ( iota_ w  e.  ( CC  ^m  ( 1 ... n ) ) ( v (  + cv `  n ) w )  =  u ) ) )
Colors of variables: wff set class
This definition is referenced by:  issubcv  25670
  Copyright terms: Public domain W3C validator