Theorem frlmnzcoordcl2

Description: The first nonzero coordinate is a scalar. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Hypotheses	frlmnzcoordcl.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)$$
	frlmnzcoordcl.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	frlmnzcoordcl.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	frlmnzcoordcl.k	$$⊢\phi \to K\in \mathrm{Ring}$$
	frlmnzcoordcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	frlmnzcoordcl.v	$$⊢\phi \to V\in B$$
	frlmnzcoordcl2.s	$$⊢S={\mathrm{Base}}_K$$
Assertion	frlmnzcoordcl2	$$⊢\phi \to V\left(J\left(V\right)\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordcl.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		frlmnzcoordcl.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
3		frlmnzcoordcl.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
4		frlmnzcoordcl.k	$$⊢\phi \to K\in \mathrm{Ring}$$
5		frlmnzcoordcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		frlmnzcoordcl.v	$$⊢\phi \to V\in B$$
7		frlmnzcoordcl2.s	$$⊢S={\mathrm{Base}}_K$$
8		ovexd	$$⊢\phi \to \left(0\dots N\right)\in \mathrm{V}$$
9		difss	$$⊢{\mathrm{Base}}_W\setminus \left\{0_W\right\}\subseteq {\mathrm{Base}}_W$$
10	3 9	eqsstri	$$⊢B\subseteq {\mathrm{Base}}_W$$
11	10 6	sselid	$$⊢\phi \to V\in {\mathrm{Base}}_W$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13	2 7 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$$
14	8 11 13	syl2anc	$$⊢\phi \to V:\left(0\dots N\right)⟶S$$
15	1 2 3 4 5 6	frlmnzcoordcl	$$⊢\phi \to J\left(V\right)\in \left(0\dots N\right)$$
16	14 15	ffvelcdmd	$$⊢\phi \to V\left(J\left(V\right)\right)\in S$$