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 )