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

Metamath Proof Explorer

Theorem uvcvv1

Description: The unit vector is one at its designated coordinate. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses uvcvv.u ⊢ U = R unitVec I
uvcvv.r ⊢ φ → R ∈ V
uvcvv.i ⊢ φ → I ∈ W
uvcvv.j ⊢ φ → J ∈ I
uvcvv1.o ⊢ 1 ˙ = 1 R
Assertion uvcvv1 ⊢ φ → U ⁡ J ⁡ J = 1 ˙

Proof

Step Hyp Ref Expression
1 uvcvv.u ⊢ U = R unitVec I
2 uvcvv.r ⊢ φ → R ∈ V
3 uvcvv.i ⊢ φ → I ∈ W
4 uvcvv.j ⊢ φ → J ∈ I
5 uvcvv1.o ⊢ 1 ˙ = 1 R
6 eqid ⊢ 0 R = 0 R
7 1 5 6 uvcvval ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ J ∈ I → U ⁡ J ⁡ J = if J = J 1 ˙ 0 R
8 2 3 4 4 7 syl31anc ⊢ φ → U ⁡ J ⁡ J = if J = J 1 ˙ 0 R
9 eqid ⊢ J = J
10 iftrue ⊢ J = J → if J = J 1 ˙ 0 R = 1 ˙
11 9 10 mp1i ⊢ φ → if J = J 1 ˙ 0 R = 1 ˙
12 8 11 eqtrd ⊢ φ → U ⁡ J ⁡ J = 1 ˙