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

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordval.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
2		frlmnzcoordval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
3		fveq1	⊢ ( 𝑏 = 𝑉 → ( 𝑏 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑖 ) )
4	3	neeq1d	⊢ ( 𝑏 = 𝑉 → ( ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ↔ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ) )
5	4	rabbidv	⊢ ( 𝑏 = 𝑉 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } = { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
6	5	infeq1d	⊢ ( 𝑏 = 𝑉 → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
7		ltso	⊢ < Or ℝ
8	7	infex	⊢ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ V
9	8	a1i	⊢ ( 𝜑 → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ V )
10	1 6 2 9	fvmptd3	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )