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	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspnnorm.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
	prjspnnorm.f	⊢ 𝐹 = ( 𝑣 ∈ 𝐵 ↦ ( ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) · 𝑣 ) )
	prjspnnorm.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	prjspnnorm.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	prjspnnorm.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
	prjspnnorm.i	⊢ 𝐼 = ( invr ‘ 𝐾 )
	prjspnnorm.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	prjspnnorm.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
	prjspnnorm.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	prjspnnorm.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	prjspnequivnorm	⊢ ( 𝜑 → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		prjspnnorm.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspnnorm.j	⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
3		prjspnnorm.f	⊢ 𝐹 = ( 𝑣 ∈ 𝐵 ↦ ( ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) · 𝑣 ) )
4		prjspnnorm.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
5		prjspnnorm.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
6		prjspnnorm.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
7		prjspnnorm.i	⊢ 𝐼 = ( invr ‘ 𝐾 )
8		prjspnnorm.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
9		prjspnnorm.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
10		prjspnnorm.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		prjspnnorm.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12	1 4 5 6 8 9	prjspner	⊢ ( 𝜑 → ∼ Er 𝐵 )
13		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
14	9	drngringd	⊢ ( 𝜑 → 𝐾 ∈ Ring )
15	2 4 5 14 10 11 6	frlmnzcoordcl2	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ∈ 𝑆 )
16	2 4 5 14 10 11	frlmnzcoordn0	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ≠ ( 0g ‘ 𝐾 ) )
17	6 13 7 9 15 16	drnginvrcld	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ∈ 𝑆 )
18	6 13 7 9 15 16	drnginvrn0d	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ≠ ( 0g ‘ 𝐾 ) )
19	1 4 5 6 8 13 9 11 17 18	prjspnvs	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ) · 𝑋 ) ∼ 𝑋 )
20	12 19	ersym	⊢ ( 𝜑 → 𝑋 ∼ ( ( 𝐼 ‘ ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ) · 𝑋 ) )
21	3 11	prjspnnormval	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐼 ‘ ( 𝑋 ‘ ( 𝐽 ‘ 𝑋 ) ) ) · 𝑋 ) )
22	20 21	breqtrrd	⊢ ( 𝜑 → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )