frlm0vald

Description: All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024)

Step	Hyp	Ref	Expression
1		frlm0vald.f	$⊢ F = R freeLMod I$
2		frlm0vald.0	$⊢ \underset{˙}{0} = 0_{R}$
3		frlm0vald.r	$⊢ φ \to R \in Ring$
4		frlm0vald.i	$⊢ φ \to I \in W$
5		frlm0vald.j	$⊢ φ \to J \in I$
6	1 2	frlm0	$⊢ (R \in Ring \land I \in W) \to I \times \{\underset{˙}{0}\} = 0_{F}$
7	3 4 6	syl2anc	$⊢ φ \to I \times \{\underset{˙}{0}\} = 0_{F}$
8	7	fveq1d	$⊢ φ \to (I \times \{\underset{˙}{0}\}) (J) = 0_{F} (J)$
9	2	fvexi	$⊢ \underset{˙}{0} \in V$
10	9	fvconst2	$⊢ J \in I \to (I \times \{\underset{˙}{0}\}) (J) = \underset{˙}{0}$
11	5 10	syl	$⊢ φ \to (I \times \{\underset{˙}{0}\}) (J) = \underset{˙}{0}$
12	8 11	eqtr3d	$⊢ φ \to 0_{F} (J) = \underset{˙}{0}$

Metamath Proof Explorer