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 ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
uvcvv.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
uvcvv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
uvcvv.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
uvcvv1.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion uvcvv1 ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐽 ) = 1 )

Proof

Step Hyp Ref Expression
1 uvcvv.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2 uvcvv.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
3 uvcvv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4 uvcvv.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
5 uvcvv1.o ⊢ 1 = ( 1r ‘ 𝑅 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 1 5 6 uvcvval ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐽 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐽 ) = if ( 𝐽 = 𝐽 , 1 , ( 0g ‘ 𝑅 ) ) )
8 2 3 4 4 7 syl31anc ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐽 ) = if ( 𝐽 = 𝐽 , 1 , ( 0g ‘ 𝑅 ) ) )
9 eqid ⊢ 𝐽 = 𝐽
10 iftrue ⊢ ( 𝐽 = 𝐽 → if ( 𝐽 = 𝐽 , 1 , ( 0g ‘ 𝑅 ) ) = 1 )
11 9 10 mp1i ⊢ ( 𝜑 → if ( 𝐽 = 𝐽 , 1 , ( 0g ‘ 𝑅 ) ) = 1 )
12 8 11 eqtrd ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐽 ) = 1 )