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

Definition df-mulcv 25680
Description: Multiplication of complex vectors by a scalar in a space of dimension  n. Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-mulcv  |-  . cv  =  ( n  e.  NN  |->  ( s  e.  CC ,  u  e.  ( CC  ^m  (
1 ... n ) ) 
|->  ( x  e.  ( 1 ... n ) 
|->  ( s  x.  (
u `  x )
) ) ) )
Distinct variable group:    n, s, u, x

Detailed syntax breakdown of Definition df-mulcv
StepHypRef Expression
1 csmcv 25679 . 2  class  . cv
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 vs . . . 4  set  s
5 vu . . . 4  set  u
6 cc 8735 . . . 4  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 ) )
13 vx . . . . 5  set  x
144cv 1622 . . . . . 6  class  s
1513cv 1622 . . . . . . 7  class  x
165cv 1622 . . . . . . 7  class  u
1715, 16cfv 5255 . . . . . 6  class  ( u `
 x )
18 cmul 8742 . . . . . 6  class  x.
1914, 17, 18co 5858 . . . . 5  class  ( s  x.  ( u `  x ) )
2013, 10, 19cmpt 4077 . . . 4  class  ( x  e.  ( 1 ... n )  |->  ( s  x.  ( u `  x ) ) )
214, 5, 6, 12, 20cmpt2 5860 . . 3  class  ( s  e.  CC ,  u  e.  ( CC  ^m  (
1 ... n ) ) 
|->  ( x  e.  ( 1 ... n ) 
|->  ( s  x.  (
u `  x )
) ) )
222, 3, 21cmpt 4077 . 2  class  ( n  e.  NN  |->  ( s  e.  CC ,  u  e.  ( CC  ^m  (
1 ... n ) ) 
|->  ( x  e.  ( 1 ... n ) 
|->  ( s  x.  (
u `  x )
) ) ) )
231, 22wceq 1623 1  wff  . cv  =  ( n  e.  NN  |->  ( s  e.  CC ,  u  e.  ( CC  ^m  (
1 ... n ) ) 
|->  ( x  e.  ( 1 ... n ) 
|->  ( s  x.  (
u `  x )
) ) ) )
Colors of variables: wff set class
This definition is referenced by:  ismulcv  25681  fnmulcv  25684
  Copyright terms: Public domain W3C validator