Theorem frlmnzcoordcl2

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

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

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordcl.j	|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
2		frlmnzcoordcl.w	|- W = ( K freeLMod ( 0 ... N ) )
3		frlmnzcoordcl.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
4		frlmnzcoordcl.k	|- ( ph -> K e. Ring )
5		frlmnzcoordcl.n	|- ( ph -> N e. NN0 )
6		frlmnzcoordcl.v	|- ( ph -> V e. B )
7		frlmnzcoordcl2.s	|- S = ( Base ` K )
8		ovexd	|- ( ph -> ( 0 ... N ) e. _V )
9		difss	|- ( ( Base ` W ) \ { ( 0g ` W ) } ) C_ ( Base ` W )
10	3 9	eqsstri	|- B C_ ( Base ` W )
11	10 6	sselid	|- ( ph -> V e. ( Base ` W ) )
12		eqid	|- ( Base ` W ) = ( Base ` W )
13	2 7 12	frlmbasf	|- ( ( ( 0 ... N ) e. _V /\ V e. ( Base ` W ) ) -> V : ( 0 ... N ) --> S )
14	8 11 13	syl2anc	|- ( ph -> V : ( 0 ... N ) --> S )
15	1 2 3 4 5 6	frlmnzcoordcl	|- ( ph -> ( J ` V ) e. ( 0 ... N ) )
16	14 15	ffvelcdmd	|- ( ph -> ( V ` ( J ` V ) ) e. S )