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 . Experimental. (Contributed by FL, 29-May-2014.)
Assertion
Ref Expression
df-divcv
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-divcv
StepHypRef Expression
1 cdivcv 25691 . 2
2 vn . . 3
3 cn 9746 . . 3
4 vu . . . 4
5 vs . . . 4
6 cc 8735 . . . . 5
7 c1 8738 . . . . . 6
82cv 1622 . . . . . 6
9 cfz 10782 . . . . . 6
107, 8, 9co 5858 . . . . 5
11 cmap 6772 . . . . 5
126, 10, 11co 5858 . . . 4
13 cc0 8737 . . . . . 6
1413csn 3640 . . . . 5
156, 14cdif 3149 . . . 4
165cv 1622 . . . . . 6
17 cdiv 9423 . . . . . 6
187, 16, 17co 5858 . . . . 5
194cv 1622 . . . . 5
20 csmcv 25679 . . . . . 6
218, 20cfv 5255 . . . . 5
2218, 19, 21co 5858 . . . 4
234, 5, 12, 15, 22cmpt2 5860 . . 3
242, 3, 23cmpt 4077 . 2
251, 24wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  isdivcv2  25693
 Copyright terms: Public domain W3C validator