This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )