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 = r ∈ V , i ∈ V ⟼ j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuvc class unitVec
1 vr setvar r
2 cvv class V
3 vi setvar i
4 vj setvar j
5 3 cv setvar i
6 vk setvar k
7 6 cv setvar k
8 4 cv setvar j
9 7 8 wceq wff k = j
10 cur class 1 r
11 1 cv setvar r
12 11 10 cfv class 1 r
13 c0g class 0 𝑔
14 11 13 cfv class 0 r
15 9 12 14 cif class if k = j 1 r 0 r
16 6 5 15 cmpt class k ∈ i ⟼ if k = j 1 r 0 r
17 4 5 16 cmpt class j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r
18 1 3 2 2 17 cmpo class r ∈ V , i ∈ V ⟼ j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r
19 0 18 wceq wff unitVec = r ∈ V , i ∈ V ⟼ j ∈ i ⟼ k ∈ i ⟼ if k = j 1 r 0 r