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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	nellindf.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	nellindf.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	nellindf.z	⊢ 0 = ( 0g ‘ 𝑊 )
	nellindf.y	⊢ 𝑌 = ( 0g ‘ 𝑅 )
	nellindf.l	⊢ 𝐿 = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
Assertion	nellindf	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ¬ 𝐹 LIndF 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		nellindf.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		nellindf.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		nellindf.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		nellindf.z	⊢ 0 = ( 0g ‘ 𝑊 )
5		nellindf.y	⊢ 𝑌 = ( 0g ‘ 𝑅 )
6		nellindf.l	⊢ 𝐿 = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
7		simpr2	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → 𝐾 ≠ ( 𝐼 × { 𝑌 } ) )
8	7	neneqd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ¬ 𝐾 = ( 𝐼 × { 𝑌 } ) )
9		simpr3	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 )
10		simpr1	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → 𝐾 ∈ 𝐿 )
11		oveq1	⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∘f · 𝐹 ) = ( 𝐾 ∘f · 𝐹 ) )
12	11	oveq2d	⊢ ( 𝑥 = 𝐾 → ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) )
13	12	eqeq1d	⊢ ( 𝑥 = 𝐾 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 ↔ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) )
14		eqeq1	⊢ ( 𝑥 = 𝐾 → ( 𝑥 = ( 𝐼 × { 𝑌 } ) ↔ 𝐾 = ( 𝐼 × { 𝑌 } ) ) )
15	13 14	imbi12d	⊢ ( 𝑥 = 𝐾 → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ( ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 → 𝐾 = ( 𝐼 × { 𝑌 } ) ) ) )
16	15	rspcv	⊢ ( 𝐾 ∈ 𝐿 → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) → ( ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 → 𝐾 = ( 𝐼 × { 𝑌 } ) ) ) )
17	10 16	syl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) → ( ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 → 𝐾 = ( 𝐼 × { 𝑌 } ) ) ) )
18	9 17	mpid	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) → 𝐾 = ( 𝐼 × { 𝑌 } ) ) )
19	8 18	mtod	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ¬ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) )
20	1 2 3 4 5 6	islindf4	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ) )
21	20	adantr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ) )
22	19 21	mtbird	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝐾 ∈ 𝐿 ∧ 𝐾 ≠ ( 𝐼 × { 𝑌 } ) ∧ ( 𝑊 Σg ( 𝐾 ∘f · 𝐹 ) ) = 0 ) ) → ¬ 𝐹 LIndF 𝑊 )