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 )