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	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
	frlmnzcoordsca.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	frlmnzcoordsca.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	frlmnzcoordsca.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	frlmnzcoordsca.z	⊢ 0 = ( 0g ‘ 𝐾 )
	frlmnzcoordsca.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
	frlmnzcoordsca.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
	frlmnzcoordsca.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	frlmnzcoordsca.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
	frlmnzcoordsca.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
	frlmnzcoordsca.0	⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion	frlmnzcoordsca	⊢ ( 𝜑 → ( 𝐽 ‘ ( 𝐶 · 𝑉 ) ) = ( 𝐽 ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordsca.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
2		frlmnzcoordsca.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		frlmnzcoordsca.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		frlmnzcoordsca.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		frlmnzcoordsca.z	⊢ 0 = ( 0g ‘ 𝐾 )
6		frlmnzcoordsca.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
7		frlmnzcoordsca.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
8		frlmnzcoordsca.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9		frlmnzcoordsca.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
10		frlmnzcoordsca.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
11		frlmnzcoordsca.0	⊢ ( 𝜑 → 𝐶 ≠ 0 )
12		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13		ovexd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... 𝑁 ) ∈ V )
14	10	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ 𝑆 )
15	9 3	eleqtrdi	⊢ ( 𝜑 → 𝑉 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
16	15	eldifad	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝑊 ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑉 ∈ ( Base ‘ 𝑊 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
19		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
20	2 12 6 13 14 17 18 4 19	frlmvscaval	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) = ( 𝐶 ( .r ‘ 𝐾 ) ( 𝑉 ‘ 𝑖 ) ) )
21	20	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝐶 ( .r ‘ 𝐾 ) ( 𝑉 ‘ 𝑖 ) ) = ( 0g ‘ 𝐾 ) ) )
22		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
23	7	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ DivRing )
24		ovexd	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
25	2 6 12	frlmbasf	⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ 𝑉 ∈ ( Base ‘ 𝑊 ) ) → 𝑉 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
26	24 16 25	syl2anc	⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
27	26	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ 𝑆 )
28	6 22 19 23 14 27	drngmul0or	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐶 ( .r ‘ 𝐾 ) ( 𝑉 ‘ 𝑖 ) ) = ( 0g ‘ 𝐾 ) ↔ ( 𝐶 = ( 0g ‘ 𝐾 ) ∨ ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) ) )
29	2	frlmsca	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
30	7 24 29	syl2anc	⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑊 ) )
31	30	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
32	5 31	eqtrid	⊢ ( 𝜑 → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
33	11 32	neeqtrd	⊢ ( 𝜑 → 𝐶 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
34	33 31	neeqtrrd	⊢ ( 𝜑 → 𝐶 ≠ ( 0g ‘ 𝐾 ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ≠ ( 0g ‘ 𝐾 ) )
36	35	neneqd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝐶 = ( 0g ‘ 𝐾 ) )
37		biorf	⊢ ( ¬ 𝐶 = ( 0g ‘ 𝐾 ) → ( ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝐶 = ( 0g ‘ 𝐾 ) ∨ ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) ) )
38	36 37	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝐶 = ( 0g ‘ 𝐾 ) ∨ ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) ) )
39	28 38	bitr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐶 ( .r ‘ 𝐾 ) ( 𝑉 ‘ 𝑖 ) ) = ( 0g ‘ 𝐾 ) ↔ ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) )
40	21 39	bitrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ↔ ( 𝑉 ‘ 𝑖 ) = ( 0g ‘ 𝐾 ) ) )
41	40	necon3bid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ↔ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ) )
42	41	rabbidva	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } = { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
43	42	infeq1d	⊢ ( 𝜑 → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
44	7	drngringd	⊢ ( 𝜑 → 𝐾 ∈ Ring )
45	2 12 6 4 44 10 16	frlmvscl	⊢ ( 𝜑 → ( 𝐶 · 𝑉 ) ∈ ( Base ‘ 𝑊 ) )
46	15	eldifsnbd	⊢ ( 𝜑 → 𝑉 ≠ ( 0g ‘ 𝑊 ) )
47		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
48		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
49		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
50		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
51	2	frlmlvec	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝑊 ∈ LVec )
52	7 24 51	syl2anc	⊢ ( 𝜑 → 𝑊 ∈ LVec )
53	30	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
54	6 53	eqtrid	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
55	10 54	eleqtrd	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
56	12 4 47 48 49 50 52 55 16	lvecvsn0	⊢ ( 𝜑 → ( ( 𝐶 · 𝑉 ) ≠ ( 0g ‘ 𝑊 ) ↔ ( 𝐶 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑉 ≠ ( 0g ‘ 𝑊 ) ) ) )
57	33 46 56	mpbir2and	⊢ ( 𝜑 → ( 𝐶 · 𝑉 ) ≠ ( 0g ‘ 𝑊 ) )
58	45 57	eldifsnd	⊢ ( 𝜑 → ( 𝐶 · 𝑉 ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
59	58 3	eleqtrrdi	⊢ ( 𝜑 → ( 𝐶 · 𝑉 ) ∈ 𝐵 )
60	1 59	frlmnzcoordval	⊢ ( 𝜑 → ( 𝐽 ‘ ( 𝐶 · 𝑉 ) ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( ( 𝐶 · 𝑉 ) ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
61	1 9	frlmnzcoordval	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
62	43 60 61	3eqtr4d	⊢ ( 𝜑 → ( 𝐽 ‘ ( 𝐶 · 𝑉 ) ) = ( 𝐽 ‘ 𝑉 ) )