Metamath Proof Explorer

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

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 fveq1 
 |-  ( b = V -> ( b ` i ) = ( V ` i ) )
4 3 neeq1d 
 |-  ( b = V -> ( ( b ` i ) =/= ( 0g ` K ) <-> ( V ` i ) =/= ( 0g ` K ) ) )
5 4 rabbidv 
 |-  ( b = V -> { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } = { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } )
6 5 infeq1d 
 |-  ( b = V -> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
7 ltso 
 |-  < Or RR
8 7 infex 
 |-  inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) e. _V
9 8 a1i 
 |-  ( ph -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) e. _V )
10 1 6 2 9 fvmptd3 
 |-  ( ph -> ( J ` V ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )