Metamath Proof Explorer

Theorem frlmnzcoordval

Description: Value of J , a function that returns the index of the first nonzero coordinate of V . (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 frlmnzcoordval ⊢ φ → J ⁡ V = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <

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 fveq1 ⊢ b = V → b ⁡ i = V ⁡ i
4 3 neeq1d ⊢ b = V → b ⁡ i ≠ 0 K ↔ V ⁡ i ≠ 0 K
5 4 rabbidv ⊢ b = V → i ∈ 0 … N | b ⁡ i ≠ 0 K = i ∈ 0 … N | V ⁡ i ≠ 0 K
6 5 infeq1d ⊢ b = V → inf i ∈ 0 … N | b ⁡ i ≠ 0 K ℝ < = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <
7 ltso ⊢ < Or ℝ
8 7 infex ⊢ inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ∈ V
9 8 a1i ⊢ φ → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ∈ V
10 1 6 2 9 fvmptd3 ⊢ φ → J ⁡ V = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <