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 ⊢ U = R unitVec I
uvcfval.o ⊢ 1 ˙ = 1 R
uvcfval.z ⊢ 0 ˙ = 0 R
Assertion uvcvval ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → U ⁡ J ⁡ K = 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 uvcval ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → U ⁡ J = k ∈ I ⟼ if k = J 1 ˙ 0 ˙
5 4 fveq1d ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I → U ⁡ J ⁡ K = k ∈ I ⟼ if k = J 1 ˙ 0 ˙ ⁡ K
6 5 adantr ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → U ⁡ J ⁡ K = k ∈ I ⟼ if k = J 1 ˙ 0 ˙ ⁡ K
7 simpr ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → K ∈ I
8 2 fvexi ⊢ 1 ˙ ∈ V
9 3 fvexi ⊢ 0 ˙ ∈ V
10 8 9 ifex ⊢ if K = J 1 ˙ 0 ˙ ∈ V
11 eqeq1 ⊢ k = K → k = J ↔ K = J
12 11 ifbid ⊢ k = K → if k = J 1 ˙ 0 ˙ = if K = J 1 ˙ 0 ˙
13 eqid ⊢ k ∈ I ⟼ if k = J 1 ˙ 0 ˙ = k ∈ I ⟼ if k = J 1 ˙ 0 ˙
14 12 13 fvmptg ⊢ K ∈ I ∧ if K = J 1 ˙ 0 ˙ ∈ V → k ∈ I ⟼ if k = J 1 ˙ 0 ˙ ⁡ K = if K = J 1 ˙ 0 ˙
15 7 10 14 sylancl ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → k ∈ I ⟼ if k = J 1 ˙ 0 ˙ ⁡ K = if K = J 1 ˙ 0 ˙
16 6 15 eqtrd ⊢ R ∈ V ∧ I ∈ W ∧ J ∈ I ∧ K ∈ I → U ⁡ J ⁡ K = if K = J 1 ˙ 0 ˙