Metamath Proof Explorer

Theorem frlmnzcoordn0

Description: The function J gives a nonzero coordinate. (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 frlmnzcoordn0 ⊢ φ → V ⁡ J ⁡ V ≠ 0 K

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 fveq2 ⊢ i = J ⁡ V → V ⁡ i = V ⁡ J ⁡ V
8 7 neeq1d ⊢ i = J ⁡ V → V ⁡ i ≠ 0 K ↔ V ⁡ J ⁡ V ≠ 0 K
9 1 6 frlmnzcoordval ⊢ φ → J ⁡ V = inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ <
10 ltso ⊢ < Or ℝ
11 10 a1i ⊢ φ → < Or ℝ
12 fzfid ⊢ φ → 0 … N ∈ Fin
13 ssrab2 ⊢ i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ 0 … N
14 13 a1i ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ 0 … N
15 12 14 ssfid ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ∈ Fin
16 2 3 4 5 6 frlmnzcoordex ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ≠ ∅
17 fzssre ⊢ 0 … N ⊆ ℝ
18 14 17 sstrdi ⊢ φ → i ∈ 0 … N | V ⁡ i ≠ 0 K ⊆ ℝ
19 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
20 11 15 16 18 19 syl13anc ⊢ φ → inf i ∈ 0 … N | V ⁡ i ≠ 0 K ℝ < ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K
21 9 20 eqeltrd ⊢ φ → J ⁡ V ∈ i ∈ 0 … N | V ⁡ i ≠ 0 K
22 8 21 elrabrd ⊢ φ → V ⁡ J ⁡ V ≠ 0 K