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=\left(b\in B⟼inf\left(\left\{i\in \left(0\dots N\right)|b\left(i\right)\ne 0_K\right\},ℝ,<\right)\right)$$
	frlmnzcoordsca.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	frlmnzcoordsca.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	frlmnzcoordsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	frlmnzcoordsca.z	$$⊢\underset{\dot{}}{0}=0_K$$
	frlmnzcoordsca.s	$$⊢S={\mathrm{Base}}_K$$
	frlmnzcoordsca.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
	frlmnzcoordsca.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	frlmnzcoordsca.v	$$⊢\phi \to V\in B$$
	frlmnzcoordsca.c	$$⊢\phi \to C\in S$$
	frlmnzcoordsca.0	$$⊢\phi \to C\ne \underset{\dot{}}{0}$$
Assertion	frlmnzcoordsca	$$⊢\phi \to J\left(C\underset{\dot{}}{·}V\right)=J\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordsca.j	$$⊢J=\left(b\in B⟼inf\left(\left\{i\in \left(0\dots N\right)|b\left(i\right)\ne 0_K\right\},ℝ,<\right)\right)$$
2		frlmnzcoordsca.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		frlmnzcoordsca.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		frlmnzcoordsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		frlmnzcoordsca.z	$$⊢\underset{\dot{}}{0}=0_K$$
6		frlmnzcoordsca.s	$$⊢S={\mathrm{Base}}_K$$
7		frlmnzcoordsca.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
8		frlmnzcoordsca.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		frlmnzcoordsca.v	$$⊢\phi \to V\in B$$
10		frlmnzcoordsca.c	$$⊢\phi \to C\in S$$
11		frlmnzcoordsca.0	$$⊢\phi \to C\ne \underset{\dot{}}{0}$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13		ovexd	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(0\dots N\right)\in \mathrm{V}$$
14	10	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to C\in S$$
15	9 3	eleqtrdi	$$⊢\phi \to V\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
16	15	eldifad	$$⊢\phi \to V\in {\mathrm{Base}}_W$$
17	16	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to V\in {\mathrm{Base}}_W$$
18		simpr	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to i\in \left(0\dots N\right)$$
19		eqid	$$⊢{\cdot }_K={\cdot }_K$$
20	2 12 6 13 14 17 18 4 19	frlmvscaval	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(C\underset{\dot{}}{·}V\right)\left(i\right)=C{\cdot }_{K}V\left(i\right)$$
21	20	eqeq1d	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(\left(C\underset{\dot{}}{·}V\right)\left(i\right)=0_K\leftrightarrow C{\cdot }_{K}V\left(i\right)=0_K\right)$$
22		eqid	$$⊢0_K=0_K$$
23	7	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to K\in \mathrm{DivRing}$$
24		ovexd	$$⊢\phi \to \left(0\dots N\right)\in \mathrm{V}$$
25	2 6 12	frlmbasf	$$⊢\left(\left(0\dots N\right)\in \mathrm{V}\wedge V\in {\mathrm{Base}}_W\right)\to V:\left(0\dots N\right)⟶S$$
26	24 16 25	syl2anc	$$⊢\phi \to V:\left(0\dots N\right)⟶S$$
27	26	ffvelcdmda	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to V\left(i\right)\in S$$
28	6 22 19 23 14 27	drngmul0or	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(C{\cdot }_{K}V\left(i\right)=0_K\leftrightarrow \left(C=0_K\vee V\left(i\right)=0_K\right)\right)$$
29	2	frlmsca	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to K=\mathrm{Scalar}\left(W\right)$$
30	7 24 29	syl2anc	$$⊢\phi \to K=\mathrm{Scalar}\left(W\right)$$
31	30	fveq2d	$$⊢\phi \to 0_K=0_{\mathrm{Scalar}\left(W\right)}$$
32	5 31	eqtrid	$$⊢\phi \to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(W\right)}$$
33	11 32	neeqtrd	$$⊢\phi \to C\ne 0_{\mathrm{Scalar}\left(W\right)}$$
34	33 31	neeqtrrd	$$⊢\phi \to C\ne 0_K$$
35	34	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to C\ne 0_K$$
36	35	neneqd	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \neg C=0_K$$
37		biorf	$$⊢\neg C=0_K\to \left(V\left(i\right)=0_K\leftrightarrow \left(C=0_K\vee V\left(i\right)=0_K\right)\right)$$
38	36 37	syl	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(V\left(i\right)=0_K\leftrightarrow \left(C=0_K\vee V\left(i\right)=0_K\right)\right)$$
39	28 38	bitr4d	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(C{\cdot }_{K}V\left(i\right)=0_K\leftrightarrow V\left(i\right)=0_K\right)$$
40	21 39	bitrd	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(\left(C\underset{\dot{}}{·}V\right)\left(i\right)=0_K\leftrightarrow V\left(i\right)=0_K\right)$$
41	40	necon3bid	$$⊢\left(\phi \wedge i\in \left(0\dots N\right)\right)\to \left(\left(C\underset{\dot{}}{·}V\right)\left(i\right)\ne 0_K\leftrightarrow V\left(i\right)\ne 0_K\right)$$
42	41	rabbidva	$$⊢\phi \to \left\{i\in \left(0\dots N\right)|\left(C\underset{\dot{}}{·}V\right)\left(i\right)\ne 0_K\right\}=\left\{i\in \left(0\dots N\right)|V\left(i\right)\ne 0_K\right\}$$
43	42	infeq1d	$$⊢\phi \to inf\left(\left\{i\in \left(0\dots N\right)|\left(C\underset{\dot{}}{·}V\right)\left(i\right)\ne 0_K\right\},ℝ,<\right)=inf\left(\left\{i\in \left(0\dots N\right)|V\left(i\right)\ne 0_K\right\},ℝ,<\right)$$
44	7	drngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
45	2 12 6 4 44 10 16	frlmvscl	$$⊢\phi \to C\underset{\dot{}}{·}V\in {\mathrm{Base}}_W$$
46	15	eldifsnbd	$$⊢\phi \to V\ne 0_W$$
47		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
48		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
49		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
50		eqid	$$⊢0_W=0_W$$
51	2	frlmlvec	$$⊢\left(K\in \mathrm{DivRing}\wedge \left(0\dots N\right)\in \mathrm{V}\right)\to W\in \mathrm{LVec}$$
52	7 24 51	syl2anc	$$⊢\phi \to W\in \mathrm{LVec}$$
53	30	fveq2d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
54	6 53	eqtrid	$$⊢\phi \to S={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
55	10 54	eleqtrd	$$⊢\phi \to C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
56	12 4 47 48 49 50 52 55 16	lvecvsn0	$$⊢\phi \to \left(C\underset{\dot{}}{·}V\ne 0_W\leftrightarrow \left(C\ne 0_{\mathrm{Scalar}\left(W\right)}\wedge V\ne 0_W\right)\right)$$
57	33 46 56	mpbir2and	$$⊢\phi \to C\underset{\dot{}}{·}V\ne 0_W$$
58	45 57	eldifsnd	$$⊢\phi \to C\underset{\dot{}}{·}V\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)$$
59	58 3	eleqtrrdi	$$⊢\phi \to C\underset{\dot{}}{·}V\in B$$
60	1 59	frlmnzcoordval	$$⊢\phi \to J\left(C\underset{\dot{}}{·}V\right)=inf\left(\left\{i\in \left(0\dots N\right)|\left(C\underset{\dot{}}{·}V\right)\left(i\right)\ne 0_K\right\},ℝ,<\right)$$
61	1 9	frlmnzcoordval	$$⊢\phi \to J\left(V\right)=inf\left(\left\{i\in \left(0\dots N\right)|V\left(i\right)\ne 0_K\right\},ℝ,<\right)$$
62	43 60 61	3eqtr4d	$$⊢\phi \to J\left(C\underset{\dot{}}{·}V\right)=J\left(V\right)$$