Database
BASIC LINEAR ALGEBRA
Vectors and free modules
Standard basis (unit vectors)
uvcvvcl2
Next ⟩
uvcvv1
Metamath Proof Explorer
Ascii
Unicode
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