Theorem uvcval

Description: Value of a single unit vector 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	uvcval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) = ( 𝑘 ∈ 𝐼 ↦ 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	uvcfval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) )
5	4	fveq1d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑈 ‘ 𝐽 ) = ( ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) ‘ 𝐽 ) )
6	5	3adant3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) = ( ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) ‘ 𝐽 ) )
7		eqid	⊢ ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) = ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) )
8		eqeq2	⊢ ( 𝑗 = 𝐽 → ( 𝑘 = 𝑗 ↔ 𝑘 = 𝐽 ) )
9	8	ifbid	⊢ ( 𝑗 = 𝐽 → if ( 𝑘 = 𝑗 , 1 , 0 ) = if ( 𝑘 = 𝐽 , 1 , 0 ) )
10	9	mpteq2dv	⊢ ( 𝑗 = 𝐽 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) )
11		simp3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → 𝐽 ∈ 𝐼 )
12		mptexg	⊢ ( 𝐼 ∈ 𝑊 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ∈ V )
13	12	3ad2ant2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ∈ V )
14	7 10 11 13	fvmptd3	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( ( 𝑗 ∈ 𝐼 ↦ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑗 , 1 , 0 ) ) ) ‘ 𝐽 ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) )
15	6 14	eqtrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) )