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 ⊢ U = R unitVec I
uvcfval.o ⊢ 1 ˙ = 1 R
uvcfval.z ⊢ 0 ˙ = 0 R
Assertion uvcval ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → U ⁡ J = k ∈ I ⟼ if k = J 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 uvcfval.u ⊢ U = R unitVec I
2 uvcfval.o ⊢ 1 ˙ = 1 R
3 uvcfval.z ⊢ 0 ˙ = 0 R
4 1 2 3 uvcfval ⊢ R ∈ V ∧ I ∈ W → U = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙
5 4 fveq1d ⊢ R ∈ V ∧ I ∈ W → U ⁡ J = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙ ⁡ J
6 5 3adant3 ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → U ⁡ J = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙ ⁡ J
7 eqid ⊢ j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙ = j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙
8 eqeq2 ⊢ j = J → k = j ↔ k = J
9 8 ifbid ⊢ j = J → if k = j 1 ˙ 0 ˙ = if k = J 1 ˙ 0 ˙
10 9 mpteq2dv ⊢ j = J → k ∈ I ⟼ if k = j 1 ˙ 0 ˙ = k ∈ I ⟼ if k = J 1 ˙ 0 ˙
11 simp3 ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → J ∈ I
12 mptexg ⊢ I ∈ W → k ∈ I ⟼ if k = J 1 ˙ 0 ˙ ∈ V
13 12 3ad2ant2 ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → k ∈ I ⟼ if k = J 1 ˙ 0 ˙ ∈ V
14 7 10 11 13 fvmptd3 ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → j ∈ I ⟼ k ∈ I ⟼ if k = j 1 ˙ 0 ˙ ⁡ J = k ∈ I ⟼ if k = J 1 ˙ 0 ˙
15 6 14 eqtrd ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → U ⁡ J = k ∈ I ⟼ if k = J 1 ˙ 0 ˙