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 20344
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 20343 . 2 class unitVec
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3340 . . 3 class V
5 vj . . . 4 setvar 𝑗
63cv 1631 . . . 4 class 𝑖
7 vk . . . . 5 setvar 𝑘
87, 5weq 2040 . . . . . 6 wff 𝑘 = 𝑗
92cv 1631 . . . . . . 7 class 𝑟
10 cur 18721 . . . . . . 7 class 1r
119, 10cfv 6049 . . . . . 6 class (1r𝑟)
12 c0g 16322 . . . . . . 7 class 0g
139, 12cfv 6049 . . . . . 6 class (0g𝑟)
148, 11, 13cif 4230 . . . . 5 class if(𝑘 = 𝑗, (1r𝑟), (0g𝑟))
157, 6, 14cmpt 4881 . . . 4 class (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))
165, 6, 15cmpt 4881 . . 3 class (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟))))
172, 3, 4, 4, 16cmpt2 6816 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
181, 17wceq 1632 1 wff unitVec = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑗𝑖 ↦ (𝑘𝑖 ↦ if(𝑘 = 𝑗, (1r𝑟), (0g𝑟)))))
Colors of variables: wff setvar class
This definition is referenced by:  uvcfval  20345
  Copyright terms: Public domain W3C validator