Theorem frlm0vald

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

	Ref	Expression
Hypotheses	frlm0vald.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlm0vald.0	$$⊢\underset{\dot{}}{0}=0_R$$
	frlm0vald.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	frlm0vald.i	$$⊢\phi \to I\in W$$
	frlm0vald.j	$$⊢\phi \to J\in I$$
Assertion	frlm0vald	$$⊢\phi \to 0_F\left(J\right)=\underset{\dot{}}{0}$$

Proof

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