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 = ( Base ` W )
	nellindf.r	|- R = ( Scalar ` W )
	nellindf.t	|- .x. = ( .s ` W )
	nellindf.z	|- .0. = ( 0g ` W )
	nellindf.y	|- Y = ( 0g ` R )
	nellindf.l	|- L = ( Base ` ( R freeLMod I ) )
Assertion	nellindf	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> -. F LIndF W )

Proof

Step	Hyp	Ref	Expression
1		nellindf.b	|- B = ( Base ` W )
2		nellindf.r	|- R = ( Scalar ` W )
3		nellindf.t	|- .x. = ( .s ` W )
4		nellindf.z	|- .0. = ( 0g ` W )
5		nellindf.y	|- Y = ( 0g ` R )
6		nellindf.l	|- L = ( Base ` ( R freeLMod I ) )
7		simpr2	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> K =/= ( I X. { Y } ) )
8	7	neneqd	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> -. K = ( I X. { Y } ) )
9		simpr3	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> ( W gsum ( K oF .x. F ) ) = .0. )
10		simpr1	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> K e. L )
11		oveq1	|- ( x = K -> ( x oF .x. F ) = ( K oF .x. F ) )
12	11	oveq2d	|- ( x = K -> ( W gsum ( x oF .x. F ) ) = ( W gsum ( K oF .x. F ) ) )
13	12	eqeq1d	|- ( x = K -> ( ( W gsum ( x oF .x. F ) ) = .0. <-> ( W gsum ( K oF .x. F ) ) = .0. ) )
14		eqeq1	|- ( x = K -> ( x = ( I X. { Y } ) <-> K = ( I X. { Y } ) ) )
15	13 14	imbi12d	|- ( x = K -> ( ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> ( ( W gsum ( K oF .x. F ) ) = .0. -> K = ( I X. { Y } ) ) ) )
16	15	rspcv	|- ( K e. L -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) -> ( ( W gsum ( K oF .x. F ) ) = .0. -> K = ( I X. { Y } ) ) ) )
17	10 16	syl	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) -> ( ( W gsum ( K oF .x. F ) ) = .0. -> K = ( I X. { Y } ) ) ) )
18	9 17	mpid	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) -> K = ( I X. { Y } ) ) )
19	8 18	mtod	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> -. A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) )
20	1 2 3 4 5 6	islindf4	|- ( ( W e. LMod /\ I e. _V /\ F : I --> B ) -> ( F LIndF W <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) ) )
21	20	adantr	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> ( F LIndF W <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) ) )
22	19 21	mtbird	|- ( ( ( W e. LMod /\ I e. _V /\ F : I --> B ) /\ ( K e. L /\ K =/= ( I X. { Y } ) /\ ( W gsum ( K oF .x. F ) ) = .0. ) ) -> -. F LIndF W )