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 ) ) ) ) )