Theorem prjspnequivnorm

Description: In a free module, a nonzero vector is equivalent to its normalized vector. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Hypotheses	prjspnnorm.e	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\right\}$$
	prjspnnorm.j	$$⊢J=\left(b\in B⟼inf\left(\left\{i\in \left(0\dots N\right)|b\left(i\right)\ne 0_K\right\},ℝ,<\right)\right)$$
	prjspnnorm.f	$$⊢F=\left(v\in B⟼I\left(v\left(J\left(v\right)\right)\right)\underset{\dot{}}{·}v\right)$$
	prjspnnorm.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
	prjspnnorm.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
	prjspnnorm.s	$$⊢S={\mathrm{Base}}_K$$
	prjspnnorm.i	$$⊢I={inv}_r\left(K\right)$$
	prjspnnorm.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	prjspnnorm.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
	prjspnnorm.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	prjspnnorm.x	$$⊢\phi \to X\in B$$
Assertion	prjspnequivnorm	$$⊢\phi \to X\underset{\dot{}}{\sim }F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		prjspnnorm.e	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \exists l\in Sx=l\underset{\dot{}}{·}y\right)\right\}$$
2		prjspnnorm.j	$$⊢J=\left(b\in B⟼inf\left(\left\{i\in \left(0\dots N\right)|b\left(i\right)\ne 0_K\right\},ℝ,<\right)\right)$$
3		prjspnnorm.f	$$⊢F=\left(v\in B⟼I\left(v\left(J\left(v\right)\right)\right)\underset{\dot{}}{·}v\right)$$
4		prjspnnorm.w	$$⊢W=K\mathrm{freeLMod}\left(0\dots N\right)$$
5		prjspnnorm.b	$$⊢B={\mathrm{Base}}_W\setminus \left\{0_W\right\}$$
6		prjspnnorm.s	$$⊢S={\mathrm{Base}}_K$$
7		prjspnnorm.i	$$⊢I={inv}_r\left(K\right)$$
8		prjspnnorm.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
9		prjspnnorm.k	$$⊢\phi \to K\in \mathrm{DivRing}$$
10		prjspnnorm.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		prjspnnorm.x	$$⊢\phi \to X\in B$$
12	1 4 5 6 8 9	prjspner	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}B$$
13		eqid	$$⊢0_K=0_K$$
14	9	drngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
15	2 4 5 14 10 11 6	frlmnzcoordcl2	$$⊢\phi \to X\left(J\left(X\right)\right)\in S$$
16	2 4 5 14 10 11	frlmnzcoordn0	$$⊢\phi \to X\left(J\left(X\right)\right)\ne 0_K$$
17	6 13 7 9 15 16	drnginvrcld	$$⊢\phi \to I\left(X\left(J\left(X\right)\right)\right)\in S$$
18	6 13 7 9 15 16	drnginvrn0d	$$⊢\phi \to I\left(X\left(J\left(X\right)\right)\right)\ne 0_K$$
19	1 4 5 6 8 13 9 11 17 18	prjspnvs	$$⊢\phi \to \left(I\left(X\left(J\left(X\right)\right)\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{\sim }X$$
20	12 19	ersym	$$⊢\phi \to X\underset{\dot{}}{\sim }\left(I\left(X\left(J\left(X\right)\right)\right)\underset{\dot{}}{·}X\right)$$
21	3 11	prjspnnormval	$$⊢\phi \to F\left(X\right)=I\left(X\left(J\left(X\right)\right)\right)\underset{\dot{}}{·}X$$
22	20 21	breqtrrd	$$⊢\phi \to X\underset{\dot{}}{\sim }F\left(X\right)$$