Metamath Proof Explorer

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 ⊢ W = K freeLMod 0 … N
frlmnzcoordex.b ⊢ B = Base W ∖ 0 W
frlmnzcoordex.k ⊢ φ → K ∈ Ring
frlmnzcoordex.n ⊢ φ → N ∈ ℕ 0
frlmnzcoordex.v ⊢ φ → V ∈ B
Assertion frlmnzcoordex ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ≠ ∅

Proof

Step Hyp Ref Expression
1 frlmnzcoordex.w ⊢ W = K freeLMod 0 … N
2 frlmnzcoordex.b ⊢ B = Base W ∖ 0 W
3 frlmnzcoordex.k ⊢ φ → K ∈ Ring
4 frlmnzcoordex.n ⊢ φ → N ∈ ℕ 0
5 frlmnzcoordex.v ⊢ φ → V ∈ B
6 5 2 eleqtrdi ⊢ φ → V ∈ Base W ∖ 0 W
7 6 eldifsnbd ⊢ φ → V ≠ 0 W
8 7 neneqd ⊢ φ → ¬ V = 0 W
9 eqid ⊢ Base W = Base W
10 ovexd ⊢ φ → 0 … N ∈ V
11 6 eldifad ⊢ φ → V ∈ Base W
12 1 9 10 11 frlmbasfn ⊢ φ → V Fn 0 … N
13 fconstfv ⊢ V : 0 … N ⟶ 0 K ↔ V Fn 0 … N ∧ ∀ i ∈ 0 … N V ⁡ i = 0 K
14 fvex ⊢ 0 K ∈ V
15 14 fconst2 ⊢ V : 0 … N ⟶ 0 K ↔ V = 0 … N × 0 K
16 13 15 sylbb1 ⊢ V Fn 0 … N ∧ ∀ i ∈ 0 … N V ⁡ i = 0 K → V = 0 … N × 0 K
17 12 16 sylan ⊢ φ ∧ ∀ i ∈ 0 … N V ⁡ i = 0 K → V = 0 … N × 0 K
18 eqid ⊢ 0 K = 0 K
19 1 18 frlm0 ⊢ K ∈ Ring ∧ 0 … N ∈ V → 0 … N × 0 K = 0 W
20 3 10 19 syl2anc ⊢ φ → 0 … N × 0 K = 0 W
21 20 adantr ⊢ φ ∧ ∀ i ∈ 0 … N V ⁡ i = 0 K → 0 … N × 0 K = 0 W
22 17 21 eqtrd ⊢ φ ∧ ∀ i ∈ 0 … N V ⁡ i = 0 K → V = 0 W
23 8 22 mtand ⊢ φ → ¬ ∀ i ∈ 0 … N V ⁡ i = 0 K
24 rabeq0 ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K = ∅ ↔ ∀ i ∈ 0 … N ¬ V ⁡ i ≠ 0 K
25 nne ⊢ ¬ V ⁡ i ≠ 0 K ↔ V ⁡ i = 0 K
26 25 ralbii ⊢ ∀ i ∈ 0 … N ¬ V ⁡ i ≠ 0 K ↔ ∀ i ∈ 0 … N V ⁡ i = 0 K
27 24 26 bitri ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K = ∅ ↔ ∀ i ∈ 0 … N V ⁡ i = 0 K
28 27 necon3abii ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ≠ ∅ ↔ ¬ ∀ i ∈ 0 … N V ⁡ i = 0 K
29 23 28 sylibr ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ≠ ∅