Theorem uvcvval

Description: Value of a unit vector coordinate in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	uvcfval.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
	uvcfval.o	⊢ 1 = ( 1r ‘ 𝑅 )
	uvcfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	uvcvval	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		uvcfval.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2		uvcfval.o	⊢ 1 = ( 1r ‘ 𝑅 )
3		uvcfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 2 3	uvcval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) )
5	4	fveq1d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) )
6	5	adantr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) )
7		simpr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → 𝐾 ∈ 𝐼 )
8	2	fvexi	⊢ 1 ∈ V
9	3	fvexi	⊢ 0 ∈ V
10	8 9	ifex	⊢ if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ V
11		eqeq1	⊢ ( 𝑘 = 𝐾 → ( 𝑘 = 𝐽 ↔ 𝐾 = 𝐽 ) )
12	11	ifbid	⊢ ( 𝑘 = 𝐾 → if ( 𝑘 = 𝐽 , 1 , 0 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) )
13		eqid	⊢ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) )
14	12 13	fvmptg	⊢ ( ( 𝐾 ∈ 𝐼 ∧ if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ V ) → ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) )
15	7 10 14	sylancl	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) )
16	6 15	eqtrd	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) )