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

Definition df-divcv 25692
Description: Division of a complex vector by a scalar in a space of dimension  n. Experimental. (Contributed by FL, 29-May-2014.)
Assertion
Ref Expression
df-divcv  |-  / cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) ,  s  e.  ( CC  \  { 0 } )  |->  ( ( 1  /  s ) ( . cv `  n
) u ) ) )
Distinct variable group:    u, n, s

Detailed syntax breakdown of Definition df-divcv
StepHypRef Expression
1 cdivcv 25691 . 2  class  / cv
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 vu . . . 4  set  u
5 vs . . . 4  set  s
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 ) )
13 cc0 8737 . . . . . 6  class  0
1413csn 3640 . . . . 5  class  { 0 }
156, 14cdif 3149 . . . 4  class  ( CC 
\  { 0 } )
165cv 1622 . . . . . 6  class  s
17 cdiv 9423 . . . . . 6  class  /
187, 16, 17co 5858 . . . . 5  class  ( 1  /  s )
194cv 1622 . . . . 5  class  u
20 csmcv 25679 . . . . . 6  class  . cv
218, 20cfv 5255 . . . . 5  class  ( . cv `  n )
2218, 19, 21co 5858 . . . 4  class  ( ( 1  /  s ) ( . cv `  n
) u )
234, 5, 12, 15, 22cmpt2 5860 . . 3  class  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  s  e.  ( CC  \  { 0 } ) 
|->  ( ( 1  / 
s ) ( . cv `  n ) u ) )
242, 3, 23cmpt 4077 . 2  class  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  s  e.  ( CC  \  { 0 } ) 
|->  ( ( 1  / 
s ) ( . cv `  n ) u ) ) )
251, 24wceq 1623 1  wff  / cv  =  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  (
1 ... n ) ) ,  s  e.  ( CC  \  { 0 } )  |->  ( ( 1  /  s ) ( . cv `  n
) u ) ) )
Colors of variables: wff set class
This definition is referenced by:  isdivcv2  25693
  Copyright terms: Public domain W3C validator