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

Definition df-uvc 19883
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 19882 . 2 class unitVec
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3172 . . 3 class V
5 vj . . . 4 setvar 𝑗
63cv 1473 . . . 4 class 𝑖
7 vk . . . . 5 setvar 𝑘
87, 5weq 1860 . . . . . 6 wff 𝑘 = 𝑗
92cv 1473 . . . . . . 7 class 𝑟
10 cur 18270 . . . . . . 7 class 1r
119, 10cfv 5790 . . . . . 6 class (1r𝑟)
12 c0g 15869 . . . . . . 7 class 0g
139, 12cfv 5790 . . . . . 6 class (0g𝑟)
148, 11, 13cif 4035 . . . . 5 class if(𝑘 = 𝑗, (1r𝑟), (0g𝑟))
157, 6, 14cmpt 4637 . . . 4 class (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))
165, 6, 15cmpt 4637 . . 3 class (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟))))
172, 3, 4, 4, 16cmpt2 6529 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
181, 17wceq 1474 1 wff unitVec = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
Colors of variables: wff setvar class
This definition is referenced by:  uvcfval  19884
  Copyright terms: Public domain W3C validator