Metamath Proof Explorer


Theorem uvcvvcl2

Description: A unit vector coordinate is a ring element. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses uvcvvcl2.u U = R unitVec I
uvcvvcl2.b B = Base R
uvcvvcl2.r φ R Ring
uvcvvcl2.i φ I W
uvcvvcl2.j φ J I
uvcvvcl2.k φ K I
Assertion uvcvvcl2 φ U J K B

Proof

Step Hyp Ref Expression
1 uvcvvcl2.u U = R unitVec I
2 uvcvvcl2.b B = Base R
3 uvcvvcl2.r φ R Ring
4 uvcvvcl2.i φ I W
5 uvcvvcl2.j φ J I
6 uvcvvcl2.k φ K I
7 eqid 1 R = 1 R
8 eqid 0 R = 0 R
9 1 7 8 uvcvval R Ring I W J I K I U J K = if K = J 1 R 0 R
10 3 4 5 6 9 syl31anc φ U J K = if K = J 1 R 0 R
11 2 7 ringidcl R Ring 1 R B
12 2 8 ring0cl R Ring 0 R B
13 11 12 ifcld R Ring if K = J 1 R 0 R B
14 3 13 syl φ if K = J 1 R 0 R B
15 10 14 eqeltrd φ U J K B