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 ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
uvcvv.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
uvcvv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
uvcvv.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
uvcvv0.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐼 )
uvcvv0.jk ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
uvcvv0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion uvcvv0 ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = 0 )

Proof

Step Hyp Ref Expression
1 uvcvv.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2 uvcvv.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
3 uvcvv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4 uvcvv.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
5 uvcvv0.k ⊢ ( 𝜑 → 𝐾 ∈ 𝐼 )
6 uvcvv0.jk ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
7 uvcvv0.z ⊢ 0 = ( 0g ‘ 𝑅 )
8 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9 1 8 7 uvcvval ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) )
10 2 3 4 5 9 syl31anc ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) )
11 nesym ⊢ ( 𝐽 ≠ 𝐾 ↔ ¬ 𝐾 = 𝐽 )
12 6 11 sylib ⊢ ( 𝜑 → ¬ 𝐾 = 𝐽 )
13 12 iffalsed ⊢ ( 𝜑 → if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) = 0 )
14 10 13 eqtrd ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = 0 )