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 \in V, i \in V ⟼ (j \in i ⟼ (k \in i ⟼ if (k = j, 1_{r}, 0_{r}))))$

Step	Hyp	Ref	Expression
0		cuvc	$class unitVec$
1		vr	$setvar r$
2		cvv	$class V$
3		vi	$setvar i$
4		vj	$setvar j$
5	3	cv	$setvar i$
6		vk	$setvar k$
7	6	cv	$setvar k$
8	4	cv	$setvar j$
9	7 8	wceq	$wff k = j$
10		cur	$class 1_{r}$
11	1	cv	$setvar r$
12	11 10	cfv	$class 1_{r}$
13		c0g	$class 0_{𝑔}$
14	11 13	cfv	$class 0_{r}$
15	9 12 14	cif	$class if (k = j, 1_{r}, 0_{r})$
16	6 5 15	cmpt	$class (k \in i ⟼ if (k = j, 1_{r}, 0_{r}))$
17	4 5 16	cmpt	$class (j \in i ⟼ (k \in i ⟼ if (k = j, 1_{r}, 0_{r})))$
18	1 3 2 2 17	cmpo	$class (r \in V, i \in V ⟼ (j \in i ⟼ (k \in i ⟼ if (k = j, 1_{r}, 0_{r}))))$
19	0 18	wceq	$wff unitVec = (r \in V, i \in V ⟼ (j \in i ⟼ (k \in i ⟼ if (k = j, 1_{r}, 0_{r}))))$

Metamath Proof Explorer