Theorem frlmnzcoordcl2

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

	Ref	Expression
Hypotheses	frlmnzcoordcl.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
	frlmnzcoordcl.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	frlmnzcoordcl.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	frlmnzcoordcl.k	⊢ ( 𝜑 → 𝐾 ∈ Ring )
	frlmnzcoordcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	frlmnzcoordcl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
	frlmnzcoordcl2.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
Assertion	frlmnzcoordcl2	⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		frlmnzcoordcl.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
2		frlmnzcoordcl.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		frlmnzcoordcl.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		frlmnzcoordcl.k	⊢ ( 𝜑 → 𝐾 ∈ Ring )
5		frlmnzcoordcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		frlmnzcoordcl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
7		frlmnzcoordcl2.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
8		ovexd	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
9		difss	⊢ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ ( Base ‘ 𝑊 )
10	3 9	eqsstri	⊢ 𝐵 ⊆ ( Base ‘ 𝑊 )
11	10 6	sselid	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝑊 ) )
12		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13	2 7 12	frlmbasf	⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ 𝑉 ∈ ( Base ‘ 𝑊 ) ) → 𝑉 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
14	8 11 13	syl2anc	⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
15	1 2 3 4 5 6	frlmnzcoordcl	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) ∈ ( 0 ... 𝑁 ) )
16	14 15	ffvelcdmd	⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ∈ 𝑆 )