Theorem frlmnzcoordcl

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

	Ref	Expression
Hypotheses	frlmnzcoordcl.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
	frlmnzcoordcl.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	frlmnzcoordcl.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	frlmnzcoordcl.k	⊢ ( 𝜑 → 𝐾 ∈ Ring )
	frlmnzcoordcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	frlmnzcoordcl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	frlmnzcoordcl	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordcl.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
2		frlmnzcoordcl.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		frlmnzcoordcl.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		frlmnzcoordcl.k	⊢ ( 𝜑 → 𝐾 ∈ Ring )
5		frlmnzcoordcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		frlmnzcoordcl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
7	1 6	frlmnzcoordval	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
8		ssrab2	⊢ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ( 0 ... 𝑁 )
9	8	a1i	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ( 0 ... 𝑁 ) )
10		ltso	⊢ < Or ℝ
11	10	a1i	⊢ ( 𝜑 → < Or ℝ )
12		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
13	12 9	ssfid	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin )
14	2 3 4 5 6	frlmnzcoordex	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ )
15		fzssre	⊢ ( 0 ... 𝑁 ) ⊆ ℝ
16	9 15	sstrdi	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ℝ )
17		fiinfcl	⊢ ( ( < Or ℝ ∧ ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin ∧ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ ∧ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ℝ ) ) → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
18	11 13 14 16 17	syl13anc	⊢ ( 𝜑 → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
19	9 18	sseldd	⊢ ( 𝜑 → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ ( 0 ... 𝑁 ) )
20	7 19	eqeltrd	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) ∈ ( 0 ... 𝑁 ) )