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 . Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-subcatv
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-subcatv
StepHypRef Expression
1 cmcv 25664 . 2
2 vn . . 3
3 cn 9746 . . 3
4 vu . . . 4
5 vv . . . 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
135cv 1622 . . . . . . 7
14 vw . . . . . . . 8
1514cv 1622 . . . . . . 7
16 cplcv 25644 . . . . . . . 8
178, 16cfv 5255 . . . . . . 7
1813, 15, 17co 5858 . . . . . 6
194cv 1622 . . . . . 6
2018, 19wceq 1623 . . . . 5
2120, 14, 12crio 6297 . . . 4
224, 5, 12, 12, 21cmpt2 5860 . . 3
232, 3, 22cmpt 4077 . 2
241, 23wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  issubcv  25670
 Copyright terms: Public domain W3C validator