Metamath Proof Explorer


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 ˙