Metamath Proof Explorer

Theorem frlmnzcoordn0

Description: The function J gives a nonzero coordinate. (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 frlmnzcoordn0 
|- ( ph -> ( V ` ( J ` V ) ) =/= ( 0g ` K ) )

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 fveq2 
 |-  ( i = ( J ` V ) -> ( V ` i ) = ( V ` ( J ` V ) ) )
8 7 neeq1d 
 |-  ( i = ( J ` V ) -> ( ( V ` i ) =/= ( 0g ` K ) <-> ( V ` ( J ` V ) ) =/= ( 0g ` K ) ) )
9 1 6 frlmnzcoordval 
 |-  ( ph -> ( J ` V ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
10 ltso 
 |-  < Or RR
11 10 a1i 
 |-  ( ph -> < Or RR )
12 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
13 ssrab2 
 |-  { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ ( 0 ... N )
14 13 a1i 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ ( 0 ... N ) )
15 12 14 ssfid 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } e. Fin )
16 2 3 4 5 6 frlmnzcoordex 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } =/= (/) )
17 fzssre 
 |-  ( 0 ... N ) C_ RR
18 14 17 sstrdi 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } C_ RR )
19 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 ) } )
20 11 15 16 18 19 syl13anc 
 |-  ( ph -> inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } )
21 9 20 eqeltrd 
 |-  ( ph -> ( J ` V ) e. { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } )
22 8 21 elrabrd 
 |-  ( ph -> ( V ` ( J ` V ) ) =/= ( 0g ` K ) )