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 = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuvc	⊢ unitVec
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vi	⊢ 𝑖
4		vj	⊢ 𝑗
5	3	cv	⊢ 𝑖
6		vk	⊢ 𝑘
7	6	cv	⊢ 𝑘
8	4	cv	⊢ 𝑗
9	7 8	wceq	⊢ 𝑘 = 𝑗
10		cur	⊢ 1r
11	1	cv	⊢ 𝑟
12	11 10	cfv	⊢ ( 1r ‘ 𝑟 )
13		c0g	⊢ 0g
14	11 13	cfv	⊢ ( 0g ‘ 𝑟 )
15	9 12 14	cif	⊢ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) )
16	6 5 15	cmpt	⊢ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) )
17	4 5 16	cmpt	⊢ ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) )
18	1 3 2 2 17	cmpo	⊢ ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
19	0 18	wceq	⊢ unitVec = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ( 𝑘 ∈ 𝑖 ↦ if ( 𝑘 = 𝑗 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )