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	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
	prjspnnorm.j	|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
	prjspnnorm.f	|- F = ( v e. B |-> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) )
	prjspnnorm.w	|- W = ( K freeLMod ( 0 ... N ) )
	prjspnnorm.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
	prjspnnorm.s	|- S = ( Base ` K )
	prjspnnorm.i	|- I = ( invr ` K )
	prjspnnorm.t	|- .x. = ( .s ` W )
	prjspnnorm.k	|- ( ph -> K e. DivRing )
	prjspnnorm.n	|- ( ph -> N e. NN0 )
	prjspnnorm.x	|- ( ph -> X e. B )
Assertion	prjspnequivnorm	|- ( ph -> X .~ ( F ` X ) )

Proof

Step	Hyp	Ref	Expression
1		prjspnnorm.e	|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
2		prjspnnorm.j	|- J = ( b e. B |-> inf ( { i e. ( 0 ... N ) | ( b ` i ) =/= ( 0g ` K ) } , RR , < ) )
3		prjspnnorm.f	|- F = ( v e. B |-> ( ( I ` ( v ` ( J ` v ) ) ) .x. v ) )
4		prjspnnorm.w	|- W = ( K freeLMod ( 0 ... N ) )
5		prjspnnorm.b	|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
6		prjspnnorm.s	|- S = ( Base ` K )
7		prjspnnorm.i	|- I = ( invr ` K )
8		prjspnnorm.t	|- .x. = ( .s ` W )
9		prjspnnorm.k	|- ( ph -> K e. DivRing )
10		prjspnnorm.n	|- ( ph -> N e. NN0 )
11		prjspnnorm.x	|- ( ph -> X e. B )
12	1 4 5 6 8 9	prjspner	|- ( ph -> .~ Er B )
13		eqid	|- ( 0g ` K ) = ( 0g ` K )
14	9	drngringd	|- ( ph -> K e. Ring )
15	2 4 5 14 10 11 6	frlmnzcoordcl2	|- ( ph -> ( X ` ( J ` X ) ) e. S )
16	2 4 5 14 10 11	frlmnzcoordn0	|- ( ph -> ( X ` ( J ` X ) ) =/= ( 0g ` K ) )
17	6 13 7 9 15 16	drnginvrcld	|- ( ph -> ( I ` ( X ` ( J ` X ) ) ) e. S )
18	6 13 7 9 15 16	drnginvrn0d	|- ( ph -> ( I ` ( X ` ( J ` X ) ) ) =/= ( 0g ` K ) )
19	1 4 5 6 8 13 9 11 17 18	prjspnvs	|- ( ph -> ( ( I ` ( X ` ( J ` X ) ) ) .x. X ) .~ X )
20	12 19	ersym	|- ( ph -> X .~ ( ( I ` ( X ` ( J ` X ) ) ) .x. X ) )
21	3 11	prjspnnormval	|- ( ph -> ( F ` X ) = ( ( I ` ( X ` ( J ` X ) ) ) .x. X ) )
22	20 21	breqtrrd	|- ( ph -> X .~ ( F ` X ) )