Theorem frlmnzcoordex

Description: Every nonzero vector of a free module has a nonzero coordinate. (Contributed by SN, 23-Sep-2026)

	Ref	Expression
Hypotheses	frlmnzcoordex.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	frlmnzcoordex.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	frlmnzcoordex.k	⊢ ( 𝜑 → 𝐾 ∈ Ring )
	frlmnzcoordex.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	frlmnzcoordex.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	frlmnzcoordex	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordex.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
2		frlmnzcoordex.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
3		frlmnzcoordex.k	⊢ ( 𝜑 → 𝐾 ∈ Ring )
4		frlmnzcoordex.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		frlmnzcoordex.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
6	5 2	eleqtrdi	⊢ ( 𝜑 → 𝑉 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
7	6	eldifsnbd	⊢ ( 𝜑 → 𝑉 ≠ ( 0g ‘ 𝑊 ) )
8	7	neneqd	⊢ ( 𝜑 → ¬ 𝑉 = ( 0g ‘ 𝑊 ) )
9		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10		ovexd	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
11	6	eldifad	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝑊 ) )
12	1 9 10 11	frlmbasfn	⊢ ( 𝜑 → 𝑉 Fn ( 0 ... 𝑁 ) )
13		fconstfv	⊢ ( 𝑉 : ( 0 ... 𝑁 ) ⟶ { ( 0g ‘ 𝐾 ) } ↔ ( 𝑉 Fn ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) )
14		fvex	⊢ ( 0g ‘ 𝐾 ) ∈ V
15	14	fconst2	⊢ ( 𝑉 : ( 0 ... 𝑁 ) ⟶ { ( 0g ‘ 𝐾 ) } ↔ 𝑉 = ( ( 0 ... 𝑁 ) × { ( 0g ‘ 𝐾 ) } ) )
16	13 15	sylbb1	⊢ ( ( 𝑉 Fn ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) → 𝑉 = ( ( 0 ... 𝑁 ) × { ( 0g ‘ 𝐾 ) } ) )
17	12 16	sylan	⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) → 𝑉 = ( ( 0 ... 𝑁 ) × { ( 0g ‘ 𝐾 ) } ) )
18		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
19	1 18	frlm0	⊢ ( ( 𝐾 ∈ Ring ∧ ( 0 ... 𝑁 ) ∈ V ) → ( ( 0 ... 𝑁 ) × { ( 0g ‘ 𝐾 ) } ) = ( 0g ‘ 𝑊 ) )
20	3 10 19	syl2anc	⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) × { ( 0g ‘ 𝐾 ) } ) = ( 0g ‘ 𝑊 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) → ( ( 0 ... 𝑁 ) × { ( 0g ‘ 𝐾 ) } ) = ( 0g ‘ 𝑊 ) )
22	17 21	eqtrd	⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) → 𝑉 = ( 0g ‘ 𝑊 ) )
23	8 22	mtand	⊢ ( 𝜑 → ¬ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) )
24		rabeq0	⊢ ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } = ∅ ↔ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ¬ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) )
25		nne	⊢ ( ¬ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ↔ ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) )
26	25	ralbii	⊢ ( ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ¬ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ↔ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) )
27	24 26	bitri	⊢ ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } = ∅ ↔ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) )
28	27	necon3abii	⊢ ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ ↔ ¬ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) )
29	23 28	sylibr	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ )