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	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
	frlmnzcoordval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	frlmnzcoordinf	⊢ ( ( 𝜑 ∧ 𝐼 ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ) → ( 𝐽 ‘ 𝑉 ) ≤ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordval.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
2		frlmnzcoordval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
3	1 2	frlmnzcoordval	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝐼 ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ) → ( 𝐽 ‘ 𝑉 ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
5		ssrab2	⊢ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ( 0 ... 𝑁 )
6		fzssre	⊢ ( 0 ... 𝑁 ) ⊆ ℝ
7	5 6	sstri	⊢ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ℝ
8		fzfi	⊢ ( 0 ... 𝑁 ) ∈ Fin
9		ssfi	⊢ ( ( ( 0 ... 𝑁 ) ∈ Fin ∧ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ( 0 ... 𝑁 ) ) → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin )
10	8 5 9	mp2an	⊢ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin
11		infrefilb	⊢ ( ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ℝ ∧ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin ∧ 𝐼 ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ) → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ≤ 𝐼 )
12	7 10 11	mp3an12	⊢ ( 𝐼 ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ≤ 𝐼 )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝐼 ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ) → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ≤ 𝐼 )
14	4 13	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐼 ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ) → ( 𝐽 ‘ 𝑉 ) ≤ 𝐼 )