Theorem nellindf

Description: A nonzero coefficient vector whose weighted combination of F sums to the zero vector implies that F is not linearly independent. (Contributed by Jiamin Zhao, 27-Aug-2026)

	Ref	Expression
Hypotheses	nellindf.b	$$⊢B={\mathrm{Base}}_W$$
	nellindf.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	nellindf.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	nellindf.z	$$⊢\underset{\dot{}}{0}=0_W$$
	nellindf.y	$$⊢Y=0_R$$
	nellindf.l	$$⊢L={\mathrm{Base}}_{\left(R\mathrm{freeLMod}I\right)}$$
Assertion	nellindf	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \neg F\mathrm{LIndF}W$$

Proof

Step	Hyp	Ref	Expression
1		nellindf.b	$$⊢B={\mathrm{Base}}_W$$
2		nellindf.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		nellindf.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		nellindf.z	$$⊢\underset{\dot{}}{0}=0_W$$
5		nellindf.y	$$⊢Y=0_R$$
6		nellindf.l	$$⊢L={\mathrm{Base}}_{\left(R\mathrm{freeLMod}I\right)}$$
7		simpr2	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to K\ne I\times \left\{Y\right\}$$
8	7	neneqd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \neg K=I\times \left\{Y\right\}$$
9		simpr3	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}$$
10		simpr1	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to K\in L$$
11		oveq1	$$⊢x=K\to x{\underset{\dot{}}{·}}_{f}F=K{\underset{\dot{}}{·}}_{f}F$$
12	11	oveq2d	$$⊢x=K\to {\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)={\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)$$
13	12	eqeq1d	$$⊢x=K\to \left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\leftrightarrow {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)$$
14		eqeq1	$$⊢x=K\to \left(x=I\times \left\{Y\right\}\leftrightarrow K=I\times \left\{Y\right\}\right)$$
15	13 14	imbi12d	$$⊢x=K\to \left(\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)\leftrightarrow \left({\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to K=I\times \left\{Y\right\}\right)\right)$$
16	15	rspcv	$$⊢K\in L\to \left(\forall x\in L\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)\to \left({\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to K=I\times \left\{Y\right\}\right)\right)$$
17	10 16	syl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \left(\forall x\in L\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)\to \left({\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to K=I\times \left\{Y\right\}\right)\right)$$
18	9 17	mpid	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \left(\forall x\in L\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)\to K=I\times \left\{Y\right\}\right)$$
19	8 18	mtod	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \neg \forall x\in L\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)$$
20	1 2 3 4 5 6	islindf4	$$⊢\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\to \left(F\mathrm{LIndF}W\leftrightarrow \forall x\in L\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)\right)$$
21	20	adantr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \left(F\mathrm{LIndF}W\leftrightarrow \forall x\in L\left({\sum }_W\left(x{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\to x=I\times \left\{Y\right\}\right)\right)$$
22	19 21	mtbird	$$⊢\left(\left(W\in \mathrm{LMod}\wedge I\in \mathrm{V}\wedge F:I⟶B\right)\wedge \left(K\in L\wedge K\ne I\times \left\{Y\right\}\wedge {\sum }_W\left(K{\underset{\dot{}}{·}}_{f}F\right)=\underset{\dot{}}{0}\right)\right)\to \neg F\mathrm{LIndF}W$$