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=\left(v\in B⟼I\left(v\left(J\left(v\right)\right)\right)\underset{\dot{}}{·}v\right)$$
	prjspnnormval.v	$$⊢\phi \to V\in B$$
Assertion	prjspnnormval	$$⊢\phi \to F\left(V\right)=I\left(V\left(J\left(V\right)\right)\right)\underset{\dot{}}{·}V$$

Proof

Step	Hyp	Ref	Expression
1		prjspnnormval.f	$$⊢F=\left(v\in B⟼I\left(v\left(J\left(v\right)\right)\right)\underset{\dot{}}{·}v\right)$$
2		prjspnnormval.v	$$⊢\phi \to V\in B$$
3		id	$$⊢v=V\to v=V$$
4		fveq2	$$⊢v=V\to J\left(v\right)=J\left(V\right)$$
5	3 4	fveq12d	$$⊢v=V\to v\left(J\left(v\right)\right)=V\left(J\left(V\right)\right)$$
6	5	fveq2d	$$⊢v=V\to I\left(v\left(J\left(v\right)\right)\right)=I\left(V\left(J\left(V\right)\right)\right)$$
7	6 3	oveq12d	$$⊢v=V\to I\left(v\left(J\left(v\right)\right)\right)\underset{\dot{}}{·}v=I\left(V\left(J\left(V\right)\right)\right)\underset{\dot{}}{·}V$$
8		ovexd	$$⊢\phi \to I\left(V\left(J\left(V\right)\right)\right)\underset{\dot{}}{·}V\in \mathrm{V}$$
9	1 7 2 8	fvmptd3	$$⊢\phi \to F\left(V\right)=I\left(V\left(J\left(V\right)\right)\right)\underset{\dot{}}{·}V$$