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

Definition df-nullcv 25754
Description: The null vector in a space of dimension  n. Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-nullcv  |-  0 cv  =  ( n  e.  NN  |->  ( x  e.  ( 1 ... n
)  |->  0 ) )
Distinct variable group:    x, n

Detailed syntax breakdown of Definition df-nullcv
StepHypRef Expression
1 c0cv 25753 . 2  class  0 cv
2 vn . . 3  set  n
3 cn 9762 . . 3  class  NN
4 vx . . . 4  set  x
5 c1 8754 . . . . 5  class  1
62cv 1631 . . . . 5  class  n
7 cfz 10798 . . . . 5  class  ...
85, 6, 7co 5874 . . . 4  class  ( 1 ... n )
9 cc0 8753 . . . 4  class  0
104, 8, 9cmpt 4093 . . 3  class  ( x  e.  ( 1 ... n )  |->  0 )
112, 3, 10cmpt 4093 . 2  class  ( n  e.  NN  |->  ( x  e.  ( 1 ... n )  |->  0 ) )
121, 11wceq 1632 1  wff  0 cv  =  ( n  e.  NN  |->  ( x  e.  ( 1 ... n
)  |->  0 ) )
Colors of variables: wff set class
This definition is referenced by:  isnullcv  25755  valvze  25757
  Copyright terms: Public domain W3C validator