Definition df-uvc 20122

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

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

Step	Hyp	Ref	Expression
1		cuvc 20121	. 2 class unitVec
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 3200	. . 3 class _V
5		vj	. . . 4 setvar j
6	3	cv 1482	. . . 4 class i
7		vk	. . . . 5 setvar k
8	7, 5	weq 1874	. . . . . 6 wff k = j
9	2	cv 1482	. . . . . . 7 class r
10		cur 18501	. . . . . . 7 class 1r
11	9, 10	cfv 5888	. . . . . 6 class ( 1r ` r )
12		c0g 16100	. . . . . . 7 class 0g
13	9, 12	cfv 5888	. . . . . 6 class ( 0g ` r )
14	8, 11, 13	cif 4086	. . . . 5 class if ( k = j , ( 1r ` r ) , ( 0g ` r ) )
15	7, 6, 14	cmpt 4729	. . . 4 class ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) )
16	5, 6, 15	cmpt 4729	. . 3 class ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) )
17	2, 3, 4, 4, 16	cmpt2 6652	. 2 class ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) )
18	1, 17	wceq 1483	1 wff unitVec = ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) )

This definition is referenced by:  uvcfval  20123