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

Metamath Proof Explorer

Theorem uvcvv0

Description: The unit vector is zero 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
uvcvv0.k ⊢ φ → K ∈ I
uvcvv0.jk ⊢ φ → J ≠ K
uvcvv0.z ⊢ 0 ˙ = 0 R
Assertion uvcvv0 ⊢ φ → U ⁡ J ⁡ K = 0 ˙

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 uvcvv0.k ⊢ φ → K ∈ I
6 uvcvv0.jk ⊢ φ → J ≠ K
7 uvcvv0.z ⊢ 0 ˙ = 0 R
8 eqid ⊢ 1 R = 1 R
9 1 8 7 uvcvval ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → U ⁡ J ⁡ K = if K = J 1 R 0 ˙
10 2 3 4 5 9 syl31anc ⊢ φ → U ⁡ J ⁡ K = if K = J 1 R 0 ˙
11 nesym ⊢ J ≠ K ↔ ¬ K = J
12 6 11 sylib ⊢ φ → ¬ K = J
13 12 iffalsed ⊢ φ → if K = J 1 R 0 ˙ = 0 ˙
14 10 13 eqtrd ⊢ φ → U ⁡ J ⁡ K = 0 ˙