Metamath Proof Explorer

Theorem frlmnzcoordsca

Description: In a free module, scaling a vector does not change the index of its first nonzero coordinate. (Contributed by SN, 24-Sep-2026)

Ref Expression
Hypotheses frlmnzcoordsca.j 
|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
frlmnzcoordsca.w 
|- W = ( K freeLMod ( 0 ... N ) )
frlmnzcoordsca.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
frlmnzcoordsca.t 
|- .x. = ( .s ` W )
frlmnzcoordsca.z 
|- .0. = ( 0g ` K )
frlmnzcoordsca.s 
|- S = ( Base ` K )
frlmnzcoordsca.k 
|- ( ph -> K e. DivRing )
frlmnzcoordsca.n 
|- ( ph -> N e. NN0 )
frlmnzcoordsca.v 
|- ( ph -> V e. B )
frlmnzcoordsca.c 
|- ( ph -> C e. S )
frlmnzcoordsca.0 
|- ( ph -> C =/= .0. )
Assertion frlmnzcoordsca 
|- ( ph -> ( J ` ( C .x. V ) ) = ( J ` V ) )

Proof

Step Hyp Ref Expression
1 frlmnzcoordsca.j 
 |-  J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
2 frlmnzcoordsca.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
3 frlmnzcoordsca.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4 frlmnzcoordsca.t 
 |-  .x. = ( .s ` W )
5 frlmnzcoordsca.z 
 |-  .0. = ( 0g ` K )
6 frlmnzcoordsca.s 
 |-  S = ( Base ` K )
7 frlmnzcoordsca.k 
 |-  ( ph -> K e. DivRing )
8 frlmnzcoordsca.n 
 |-  ( ph -> N e. NN0 )
9 frlmnzcoordsca.v 
 |-  ( ph -> V e. B )
10 frlmnzcoordsca.c 
 |-  ( ph -> C e. S )
11 frlmnzcoordsca.0 
 |-  ( ph -> C =/= .0. )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 ovexd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( 0 ... N ) e. _V )
14 10 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> C e. S )
15 9 3 eleqtrdi 
 |-  ( ph -> V e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
16 15 eldifad 
 |-  ( ph -> V e. ( Base ` W ) )
17 16 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> V e. ( Base ` W ) )
18 simpr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) )
19 eqid 
 |-  ( .r ` K ) = ( .r ` K )
20 2 12 6 13 14 17 18 4 19 frlmvscaval 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( C .x. V ) ` i ) = ( C ( .r ` K ) ( V ` i ) ) )
21 20 eqeq1d 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( ( C .x. V ) ` i ) = ( 0g ` K ) <-> ( C ( .r ` K ) ( V ` i ) ) = ( 0g ` K ) ) )
22 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
23 7 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> K e. DivRing )
24 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
25 2 6 12 frlmbasf 
 |-  ( ( ( 0 ... N ) e. _V /\ V e. ( Base ` W ) ) -> V : ( 0 ... N ) --> S )
26 24 16 25 syl2anc 
 |-  ( ph -> V : ( 0 ... N ) --> S )
27 26 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( V ` i ) e. S )
28 6 22 19 23 14 27 drngmul0or 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( C ( .r ` K ) ( V ` i ) ) = ( 0g ` K ) <-> ( C = ( 0g ` K ) \/ ( V ` i ) = ( 0g ` K ) ) ) )
29 2 frlmsca 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> K = ( Scalar ` W ) )
30 7 24 29 syl2anc 
 |-  ( ph -> K = ( Scalar ` W ) )
31 30 fveq2d 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` ( Scalar ` W ) ) )
32 5 31 eqtrid 
 |-  ( ph -> .0. = ( 0g ` ( Scalar ` W ) ) )
33 11 32 neeqtrd 
 |-  ( ph -> C =/= ( 0g ` ( Scalar ` W ) ) )
34 33 31 neeqtrrd 
 |-  ( ph -> C =/= ( 0g ` K ) )
35 34 adantr 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> C =/= ( 0g ` K ) )
36 35 neneqd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> -. C = ( 0g ` K ) )
37 biorf 
 |-  ( -. C = ( 0g ` K ) -> ( ( V ` i ) = ( 0g ` K ) <-> ( C = ( 0g ` K ) \/ ( V ` i ) = ( 0g ` K ) ) ) )
38 36 37 syl 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( V ` i ) = ( 0g ` K ) <-> ( C = ( 0g ` K ) \/ ( V ` i ) = ( 0g ` K ) ) ) )
39 28 38 bitr4d 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( C ( .r ` K ) ( V ` i ) ) = ( 0g ` K ) <-> ( V ` i ) = ( 0g ` K ) ) )
40 21 39 bitrd 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( ( C .x. V ) ` i ) = ( 0g ` K ) <-> ( V ` i ) = ( 0g ` K ) ) )
41 40 necon3bid 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( ( C .x. V ) ` i ) =/= ( 0g ` K ) <-> ( V ` i ) =/= ( 0g ` K ) ) )
42 41 rabbidva 
 |-  ( ph -> { i e. ( 0 ... N ) | ( ( C .x. V ) ` i ) =/= ( 0g ` K ) } = { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } )
43 42 infeq1d 
 |-  ( ph -> inf ( { i e. ( 0 ... N ) | ( ( C .x. V ) ` i ) =/= ( 0g ` K ) } , RR , < ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
44 7 drngringd 
 |-  ( ph -> K e. Ring )
45 2 12 6 4 44 10 16 frlmvscl 
 |-  ( ph -> ( C .x. V ) e. ( Base ` W ) )
46 15 eldifsnbd 
 |-  ( ph -> V =/= ( 0g ` W ) )
47 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
48 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
49 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
50 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
51 2 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> W e. LVec )
52 7 24 51 syl2anc 
 |-  ( ph -> W e. LVec )
53 30 fveq2d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( Scalar ` W ) ) )
54 6 53 eqtrid 
 |-  ( ph -> S = ( Base ` ( Scalar ` W ) ) )
55 10 54 eleqtrd 
 |-  ( ph -> C e. ( Base ` ( Scalar ` W ) ) )
56 12 4 47 48 49 50 52 55 16 lvecvsn0 
 |-  ( ph -> ( ( C .x. V ) =/= ( 0g ` W ) <-> ( C =/= ( 0g ` ( Scalar ` W ) ) /\ V =/= ( 0g ` W ) ) ) )
57 33 46 56 mpbir2and 
 |-  ( ph -> ( C .x. V ) =/= ( 0g ` W ) )
58 45 57 eldifsnd 
 |-  ( ph -> ( C .x. V ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
59 58 3 eleqtrrdi 
 |-  ( ph -> ( C .x. V ) e. B )
60 1 59 frlmnzcoordval 
 |-  ( ph -> ( J ` ( C .x. V ) ) = inf ( { i e. ( 0 ... N ) | ( ( C .x. V ) ` i ) =/= ( 0g ` K ) } , RR , < ) )
61 1 9 frlmnzcoordval 
 |-  ( ph -> ( J ` V ) = inf ( { i e. ( 0 ... N ) | ( V ` i ) =/= ( 0g ` K ) } , RR , < ) )
62 43 60 61 3eqtr4d 
 |-  ( ph -> ( J ` ( C .x. V ) ) = ( J ` V ) )