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	|- F = ( v e. B |-> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) )
	prjspnnormval.v	|- ( ph -> V e. B )
Assertion	prjspnnormval	|- ( ph -> ( F ` V ) = ( ( I ` ( V ` ( J ` V ) ) ) .x. V ) )

Proof

Step	Hyp	Ref	Expression
1		prjspnnormval.f	|- F = ( v e. B |-> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) )
2		prjspnnormval.v	|- ( ph -> V e. B )
3		id	|- ( v = V -> v = V )
4		fveq2	|- ( v = V -> ( J ` v ) = ( J ` V ) )
5	3 4	fveq12d	|- ( v = V -> ( v ` ( J ` v ) ) = ( V ` ( J ` V ) ) )
6	5	fveq2d	|- ( v = V -> ( I ` ( v ` ( J ` v ) ) ) = ( I ` ( V ` ( J ` V ) ) ) )
7	6 3	oveq12d	|- ( v = V -> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) = ( ( I ` ( V ` ( J ` V ) ) ) .x. V ) )
8		ovexd	|- ( ph -> ( ( I ` ( V ` ( J ` V ) ) ) .x. V ) e. _V )
9	1 7 2 8	fvmptd3	|- ( ph -> ( F ` V ) = ( ( I ` ( V ` ( J ` V ) ) ) .x. V ) )