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 = ( 𝑟 ∈ 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𝑟 ) ) ) ) )