Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-uvc Structured version   Visualization version   GIF version

Definition df-uvc 19941
 Description: ((𝑅 unitVec 𝐼)‘𝑗) is the unit vector in (𝑅 freeLMod 𝐼) along the 𝑗 axis. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
df-uvc unitVec = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
Distinct variable group:   𝑖,𝑟,𝑗,𝑘

Detailed syntax breakdown of Definition df-uvc
StepHypRef Expression
1 cuvc 19940 . 2 class unitVec
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3173 . . 3 class V
5 vj . . . 4 setvar 𝑗
63cv 1474 . . . 4 class 𝑖
7 vk . . . . 5 setvar 𝑘
87, 5weq 1861 . . . . . 6 wff 𝑘 = 𝑗
92cv 1474 . . . . . . 7 class 𝑟
10 cur 18324 . . . . . . 7 class 1r
119, 10cfv 5804 . . . . . 6 class (1r𝑟)
12 c0g 15923 . . . . . . 7 class 0g
139, 12cfv 5804 . . . . . 6 class (0g𝑟)
148, 11, 13cif 4036 . . . . 5 class if(𝑘 = 𝑗, (1r𝑟), (0g𝑟))
157, 6, 14cmpt 4643 . . . 4 class (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))
165, 6, 15cmpt 4643 . . 3 class (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟))))
172, 3, 4, 4, 16cmpt2 6551 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
181, 17wceq 1475 1 wff unitVec = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
 Colors of variables: wff setvar class This definition is referenced by:  uvcfval  19942
 Copyright terms: Public domain W3C validator