This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑟 ) ) ) ) )