Metamath Proof Explorer

Definition df-uvc

Description: ( ( R unitVec I )j ) is the unit vector in ( R freeLMod I ) along the j axis. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion df-uvc 
|- unitVec = ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuvc 
 |-  unitVec
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vi 
 |-  i
4 vj 
 |-  j
5 3 cv 
 |-  i
6 vk 
 |-  k
7 6 cv 
 |-  k
8 4 cv 
 |-  j
9 7 8 wceq 
 |-  k = j
10 cur 
 |-  1r
11 1 cv 
 |-  r
12 11 10 cfv 
 |-  ( 1r ` r )
13 c0g 
 |-  0g
14 11 13 cfv 
 |-  ( 0g ` r )
15 9 12 14 cif 
 |-  if ( k = j , ( 1r ` r ) , ( 0g ` r ) )
16 6 5 15 cmpt 
 |-  ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) )
17 4 5 16 cmpt 
 |-  ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) )
18 1 3 2 2 17 cmpo 
 |-  ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) )
19 0 18 wceq 
 |-  unitVec = ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) )