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

Proof

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