Metamath Proof Explorer

Theorem frlmnzcoordinf

Description: The result ( JV ) is the smallest index corresponding to a nonzero coordinate. (Contributed by SN, 23-Sep-2026)

Ref Expression
Hypotheses frlmnzcoordval.j ⊢ J = b ∈ B ⟼ inf i ∈ 0 … N | b ⁡ i ≠ 0 K ℝ <
frlmnzcoordval.v ⊢ φ → V ∈ B
Assertion frlmnzcoordinf ⊢ φ ∧ I ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K → J ⁡ V ≤ I

Proof

Step Hyp Ref Expression
1 frlmnzcoordval.j ⊢ J = b ∈ B ⟼ inf i ∈ 0 … N | b ⁡ i ≠ 0 K ℝ <
2 frlmnzcoordval.v ⊢ φ → V ∈ B
3 1 2 frlmnzcoordval ⊢ φ → J ⁡ V = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <
4 3 adantr ⊢ φ ∧ I ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K → J ⁡ V = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <
5 ssrab2 ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ 0 … N
6 fzssre ⊢ 0 … N ⊆ ℝ
7 5 6 sstri ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ ℝ
8 fzfi ⊢ 0 … N ∈ Fin
9 ssfi ⊢ 0 … N ∈ Fin ∧ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ 0 … N → i ∈ 0 … N | V ⁡ i ≠ 0 K ∈ Fin
10 8 5 9 mp2an ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ∈ Fin
11 infrefilb ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ ℝ ∧ i ∈ 0 … N | V ⁡ i ≠ 0 K ∈ Fin ∧ I ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ≤ I
12 7 10 11 mp3an12 ⊢ I ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ≤ I
13 12 adantl ⊢ φ ∧ I ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ≤ I
14 4 13 eqbrtrd ⊢ φ ∧ I ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K → J ⁡ V ≤ I