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	|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
	frlmnzcoordval.v	|- ( ph -> V e. B )
Assertion	frlmnzcoordinf	|- ( ( ph /\ I e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } ) -> ( J ` V ) <_ I )

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordval.j	|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
2		frlmnzcoordval.v	|- ( ph -> V e. B )
3	1 2	frlmnzcoordval	|- ( ph -> ( J ` V ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
4	3	adantr	|- ( ( ph /\ I e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } ) -> ( J ` V ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
5		ssrab2	|- { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ ( 0 ... N )
6		fzssre	|- ( 0 ... N ) C_ RR
7	5 6	sstri	|- { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ RR
8		fzfi	|- ( 0 ... N ) e. Fin
9		ssfi	|- ( ( ( 0 ... N ) e. Fin /\ { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ ( 0 ... N ) ) -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } e. Fin )
10	8 5 9	mp2an	|- { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } e. Fin
11		infrefilb	|- ( ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ RR /\ { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } e. Fin /\ I e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } ) -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) <_ I )
12	7 10 11	mp3an12	|- ( I e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) <_ I )
13	12	adantl	|- ( ( ph /\ I e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } ) -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) <_ I )
14	4 13	eqbrtrd	|- ( ( ph /\ I e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } ) -> ( J ` V ) <_ I )