Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-uvc Unicode version

Definition df-uvc 27215
Description:  ( ( R unitVec  I ) `  i ) is the unit vector in  ( R freeLMod  I ) along the  i axis. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
df-uvc  |- unitVec  =  ( r  e.  _V , 
i  e.  _V  |->  ( j  e.  i  |->  ( k  e.  i  |->  if ( k  =  j ,  ( 1r `  r ) ,  ( 0g `  r ) ) ) ) )
Distinct variable group:    i, r, j, k

Detailed syntax breakdown of Definition df-uvc
StepHypRef Expression
1 cuvc 27213 . 2  class unitVec
2 vr . . 3  set  r
3 vi . . 3  set  i
4 cvv 2788 . . 3  class  _V
5 vj . . . 4  set  j
63cv 1622 . . . 4  class  i
7 vk . . . . 5  set  k
87, 5weq 1624 . . . . . 6  wff  k  =  j
92cv 1622 . . . . . . 7  class  r
10 cur 15339 . . . . . . 7  class  1r
119, 10cfv 5255 . . . . . 6  class  ( 1r
`  r )
12 c0g 13400 . . . . . . 7  class  0g
139, 12cfv 5255 . . . . . 6  class  ( 0g
`  r )
148, 11, 13cif 3565 . . . . 5  class  if ( k  =  j ,  ( 1r `  r
) ,  ( 0g
`  r ) )
157, 6, 14cmpt 4077 . . . 4  class  ( k  e.  i  |->  if ( k  =  j ,  ( 1r `  r
) ,  ( 0g
`  r ) ) )
165, 6, 15cmpt 4077 . . 3  class  ( j  e.  i  |->  ( k  e.  i  |->  if ( k  =  j ,  ( 1r `  r
) ,  ( 0g
`  r ) ) ) )
172, 3, 4, 4, 16cmpt2 5860 . 2  class  ( r  e.  _V ,  i  e.  _V  |->  ( j  e.  i  |->  ( k  e.  i  |->  if ( k  =  j ,  ( 1r `  r
) ,  ( 0g
`  r ) ) ) ) )
181, 17wceq 1623 1  wff unitVec  =  ( r  e.  _V , 
i  e.  _V  |->  ( j  e.  i  |->  ( k  e.  i  |->  if ( k  =  j ,  ( 1r `  r ) ,  ( 0g `  r ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  uvcfval  27233
  Copyright terms: Public domain W3C validator