Theorem prjspnnormval

Description: Value of F , a function that 'normalizes' a vector V by scaling the first nonzero coordinate to 1. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Hypotheses	prjspnnormval.f	⊢ 𝐹 = ( 𝑣 ∈ 𝐵 ↦ ( ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) · 𝑣 ) )
	prjspnnormval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	prjspnnormval	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑉 ) = ( ( 𝐼 ‘ ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ) · 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		prjspnnormval.f	⊢ 𝐹 = ( 𝑣 ∈ 𝐵 ↦ ( ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) · 𝑣 ) )
2		prjspnnormval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
3		id	⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
4		fveq2	⊢ ( 𝑣 = 𝑉 → ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑉 ) )
5	3 4	fveq12d	⊢ ( 𝑣 = 𝑉 → ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) = ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) )
6	5	fveq2d	⊢ ( 𝑣 = 𝑉 → ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) = ( 𝐼 ‘ ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ) )
7	6 3	oveq12d	⊢ ( 𝑣 = 𝑉 → ( ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) · 𝑣 ) = ( ( 𝐼 ‘ ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ) · 𝑉 ) )
8		ovexd	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ) · 𝑉 ) ∈ V )
9	1 7 2 8	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑉 ) = ( ( 𝐼 ‘ ( 𝑉 ‘ ( 𝐽 ‘ 𝑉 ) ) ) · 𝑉 ) )