Metamath Proof Explorer

Theorem frlmnzcoordcl

Description: Closure of the first nonzero coordinate function J . (Contributed by SN, 23-Sep-2026)

Ref Expression
Hypotheses frlmnzcoordcl.j ⊢ J = b ∈ B ⟼ inf i ∈ 0 … N | b ⁡ i ≠ 0 K ℝ <
frlmnzcoordcl.w ⊢ W = K freeLMod 0 … N
frlmnzcoordcl.b ⊢ B = Base W ∖ 0 W
frlmnzcoordcl.k ⊢ φ → K ∈ Ring
frlmnzcoordcl.n ⊢ φ → N ∈ ℕ 0
frlmnzcoordcl.v ⊢ φ → V ∈ B
Assertion frlmnzcoordcl ⊢ φ → J ⁡ V ∈ 0 … N

Proof

Step Hyp Ref Expression
1 frlmnzcoordcl.j ⊢ J = b ∈ B ⟼ inf i ∈ 0 … N | b ⁡ i ≠ 0 K ℝ <
2 frlmnzcoordcl.w ⊢ W = K freeLMod 0 … N
3 frlmnzcoordcl.b ⊢ B = Base W ∖ 0 W
4 frlmnzcoordcl.k ⊢ φ → K ∈ Ring
5 frlmnzcoordcl.n ⊢ φ → N ∈ ℕ 0
6 frlmnzcoordcl.v ⊢ φ → V ∈ B
7 1 6 frlmnzcoordval ⊢ φ → J ⁡ V = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <
8 ssrab2 ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ 0 … N
9 8 a1i ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ 0 … N
10 ltso ⊢ < Or ℝ
11 10 a1i ⊢ φ → < Or ℝ
12 fzfid ⊢ φ → 0 … N ∈ Fin
13 12 9 ssfid ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ∈ Fin
14 2 3 4 5 6 frlmnzcoordex ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ≠ ∅
15 fzssre ⊢ 0 … N ⊆ ℝ
16 9 15 sstrdi ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ ℝ
17 fiinfcl ⊢ < Or ℝ ∧ i ∈ 0 … N | V ⁡ i ≠ 0 K ∈ Fin ∧ i ∈ 0 … N | V ⁡ i ≠ 0 K ≠ ∅ ∧ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ ℝ → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K
18 11 13 14 16 17 syl13anc ⊢ φ → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K
19 9 18 sseldd ⊢ φ → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ∈ 0 … N
20 7 19 eqeltrd ⊢ φ → J ⁡ V ∈ 0 … N