Metamath Proof Explorer

Theorem frlmnzcoordex

Description: Every nonzero vector of a free module has a nonzero coordinate. (Contributed by SN, 23-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 frlmnzcoordex.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
2 frlmnzcoordex.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
3 frlmnzcoordex.k 
 |-  ( ph -> K e. Ring )
4 frlmnzcoordex.n 
 |-  ( ph -> N e. NN0 )
5 frlmnzcoordex.v 
 |-  ( ph -> V e. B )
6 5 2 eleqtrdi 
 |-  ( ph -> V e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
7 6 eldifsnbd 
 |-  ( ph -> V =/= ( 0g ` W ) )
8 7 neneqd 
 |-  ( ph -> -. V = ( 0g ` W ) )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
11 6 eldifad 
 |-  ( ph -> V e. ( Base ` W ) )
12 1 9 10 11 frlmbasfn 
 |-  ( ph -> V Fn ( 0 ... N ) )
13 fconstfv 
 |-  ( V : ( 0 ... N ) --> { ( 0g ` K ) } <-> ( V Fn ( 0 ... N ) /\ A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) ) )
14 fvex 
 |-  ( 0g ` K ) e. _V
15 14 fconst2 
 |-  ( V : ( 0 ... N ) --> { ( 0g ` K ) } <-> V = ( ( 0 ... N ) X. { ( 0g ` K ) } ) )
16 13 15 sylbb1 
 |-  ( ( V Fn ( 0 ... N ) /\ A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) ) -> V = ( ( 0 ... N ) X. { ( 0g ` K ) } ) )
17 12 16 sylan 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) ) -> V = ( ( 0 ... N ) X. { ( 0g ` K ) } ) )
18 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
19 1 18 frlm0 
 |-  ( ( K e. Ring /\ ( 0 ... N ) e. _V ) -> ( ( 0 ... N ) X. { ( 0g ` K ) } ) = ( 0g ` W ) )
20 3 10 19 syl2anc 
 |-  ( ph -> ( ( 0 ... N ) X. { ( 0g ` K ) } ) = ( 0g ` W ) )
21 20 adantr 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) ) -> ( ( 0 ... N ) X. { ( 0g ` K ) } ) = ( 0g ` W ) )
22 17 21 eqtrd 
 |-  ( ( ph /\ A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) ) -> V = ( 0g ` W ) )
23 8 22 mtand 
 |-  ( ph -> -. A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) )
24 rabeq0 
 |-  ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } = (/) <-> A. i e. ( 0 ... N ) -. ( V ` i ) =/= ( 0g ` K ) )
25 nne 
 |-  ( -. ( V ` i ) =/= ( 0g ` K ) <-> ( V ` i ) = ( 0g ` K ) )
26 25 ralbii 
 |-  ( A. i e. ( 0 ... N ) -. ( V ` i ) =/= ( 0g ` K ) <-> A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) )
27 24 26 bitri 
 |-  ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } = (/) <-> A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) )
28 27 necon3abii 
 |-  ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } =/= (/) <-> -. A. i e. ( 0 ... N ) ( V ` i ) = ( 0g ` K ) )
29 23 28 sylibr 
 |-  ( ph -> { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } =/= (/) )