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 25795
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 25794 . 2  class  / cv
2 vn . . 3  set  n
3 cn 9762 . . 3  class  NN
4 vu . . . 4  set  u
5 vs . . . 4  set  s
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 cc0 8753 . . . . . 6  class  0
1413csn 3653 . . . . 5  class  { 0 }
156, 14cdif 3162 . . . 4  class  ( CC 
\  { 0 } )
165cv 1631 . . . . . 6  class  s
17 cdiv 9439 . . . . . 6  class  /
187, 16, 17co 5874 . . . . 5  class  ( 1  /  s )
194cv 1631 . . . . 5  class  u
20 csmcv 25782 . . . . . 6  class  . cv
218, 20cfv 5271 . . . . 5  class  ( . cv `  n )
2218, 19, 21co 5874 . . . 4  class  ( ( 1  /  s ) ( . cv `  n
) u )
234, 5, 12, 15, 22cmpt2 5876 . . 3  class  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  s  e.  ( CC  \  { 0 } ) 
|->  ( ( 1  / 
s ) ( . cv `  n ) u ) )
242, 3, 23cmpt 4093 . 2  class  ( n  e.  NN  |->  ( u  e.  ( CC  ^m  ( 1 ... n
) ) ,  s  e.  ( CC  \  { 0 } ) 
|->  ( ( 1  / 
s ) ( . cv `  n ) u ) ) )
251, 24wceq 1632 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  25796
  Copyright terms: Public domain W3C validator