Metamath Proof Explorer

Theorem frlmnzcoordcl

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

Ref Expression
Hypotheses frlmnzcoordcl.j 
|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
frlmnzcoordcl.w 
|- W = ( K freeLMod ( 0 ... N ) )
frlmnzcoordcl.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
frlmnzcoordcl.k 
|- ( ph -> K e. Ring )
frlmnzcoordcl.n 
|- ( ph -> N e. NN0 )
frlmnzcoordcl.v 
|- ( ph -> V e. B )
Assertion frlmnzcoordcl 
|- ( ph -> ( J ` V ) e. ( 0 ... N ) )

Proof

Step Hyp Ref Expression
1 frlmnzcoordcl.j 
 |-  J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
2 frlmnzcoordcl.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
3 frlmnzcoordcl.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4 frlmnzcoordcl.k 
 |-  ( ph -> K e. Ring )
5 frlmnzcoordcl.n 
 |-  ( ph -> N e. NN0 )
6 frlmnzcoordcl.v 
 |-  ( ph -> V e. B )
7 1 6 frlmnzcoordval 
 |-  ( ph -> ( J ` V ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
8 ssrab2 
 |-  { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ ( 0 ... N )
9 8 a1i 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ ( 0 ... N ) )
10 ltso 
 |-  < Or RR
11 10 a1i 
 |-  ( ph -> < Or RR )
12 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
13 12 9 ssfid 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } e. Fin )
14 2 3 4 5 6 frlmnzcoordex 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } =/= (/) )
15 fzssre 
 |-  ( 0 ... N ) C_ RR
16 9 15 sstrdi 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ RR )
17 fiinfcl 
 |-  ( ( < Or RR /\ ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } e. Fin /\ { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } =/= (/) /\ { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ RR ) ) -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } )
18 11 13 14 16 17 syl13anc 
 |-  ( ph -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } )
19 9 18 sseldd 
 |-  ( ph -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) e. ( 0 ... N ) )
20 7 19 eqeltrd 
 |-  ( ph -> ( J ` V ) e. ( 0 ... N ) )