Theorem frlmnzcoordn0

Description: The function J gives a nonzero coordinate. (Contributed by SN, 23-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	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	frlmnzcoordn0	⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ≠ ( 0g ‘ 𝐾 ) )

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		fveq2	⊢ ( 𝑖 = ( 𝐽 ‘ 𝑉 ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) )
8	7	neeq1d	⊢ ( 𝑖 = ( 𝐽 ‘ 𝑉 ) → ( ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) ↔ ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ≠ ( 0g ‘ 𝐾 ) ) )
9	1 6	frlmnzcoordval	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) = inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
10		ltso	⊢ < Or ℝ
11	10	a1i	⊢ ( 𝜑 → < Or ℝ )
12		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
13		ssrab2	⊢ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ( 0 ... 𝑁 )
14	13	a1i	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ( 0 ... 𝑁 ) )
15	12 14	ssfid	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin )
16	2 3 4 5 6	frlmnzcoordex	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ )
17		fzssre	⊢ ( 0 ... 𝑁 ) ⊆ ℝ
18	14 17	sstrdi	⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ℝ )
19		fiinfcl	⊢ ( ( < Or ℝ ∧ ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ∈ Fin ∧ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ≠ ∅ ∧ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } ⊆ ℝ ) ) → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
20	11 15 16 18 19	syl13anc	⊢ ( 𝜑 → inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
21	9 20	eqeltrd	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑉 ) ∈ { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑉 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } )
22	8 21	elrabrd	⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ≠ ( 0g ‘ 𝐾 ) )