Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
frlm0vald
Next ⟩
frlmsnic
Metamath Proof Explorer
Ascii
Unicode
Theorem
frlm0vald
Description:
All coordinates of the zero vector are zero.
(Contributed by
SN
, 14-Aug-2024)
Ref
Expression
Hypotheses
frlm0vald.f
⊢
F
=
R
freeLMod
I
frlm0vald.0
⊢
0
˙
=
0
R
frlm0vald.r
⊢
φ
→
R
∈
Ring
frlm0vald.i
⊢
φ
→
I
∈
W
frlm0vald.j
⊢
φ
→
J
∈
I
Assertion
frlm0vald
⊢
φ
→
0
F
⁡
J
=
0
˙
Proof
Step
Hyp
Ref
Expression
1
frlm0vald.f
⊢
F
=
R
freeLMod
I
2
frlm0vald.0
⊢
0
˙
=
0
R
3
frlm0vald.r
⊢
φ
→
R
∈
Ring
4
frlm0vald.i
⊢
φ
→
I
∈
W
5
frlm0vald.j
⊢
φ
→
J
∈
I
6
1
2
frlm0
⊢
R
∈
Ring
∧
I
∈
W
→
I
×
0
˙
=
0
F
7
3
4
6
syl2anc
⊢
φ
→
I
×
0
˙
=
0
F
8
7
fveq1d
⊢
φ
→
I
×
0
˙
⁡
J
=
0
F
⁡
J
9
2
fvexi
⊢
0
˙
∈
V
10
9
fvconst2
⊢
J
∈
I
→
I
×
0
˙
⁡
J
=
0
˙
11
5
10
syl
⊢
φ
→
I
×
0
˙
⁡
J
=
0
˙
12
8
11
eqtr3d
⊢
φ
→
0
F
⁡
J
=
0
˙