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

Metamath Proof Explorer

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