Theorem prjspnvs

Description: A nonzero multiple of a vector is equivalent to the vector. This is prjspvs with the equivalence relation converted by prjspnerlem . (Contributed by SN, 8-Aug-2024)

	Ref	Expression
Hypotheses	prjspnvs.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspnvs.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	prjspnvs.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	prjspnvs.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
	prjspnvs.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
	prjspnvs.0	⊢ 0 = ( 0g ‘ 𝐾 )
	prjspnvs.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
	prjspnvs.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prjspnvs.2	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
	prjspnvs.3	⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion	prjspnvs	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∼ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		prjspnvs.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspnvs.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3		prjspnvs.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		prjspnvs.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
5		prjspnvs.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		prjspnvs.0	⊢ 0 = ( 0g ‘ 𝐾 )
7		prjspnvs.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
8		prjspnvs.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		prjspnvs.2	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
10		prjspnvs.3	⊢ ( 𝜑 → 𝐶 ≠ 0 )
11		ovexd	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
12	2	frlmlvec	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝑊 ∈ LVec )
13	7 11 12	syl2anc	⊢ ( 𝜑 → 𝑊 ∈ LVec )
14		nelsn	⊢ ( 𝐶 ≠ 0 → ¬ 𝐶 ∈ { 0 } )
15	10 14	syl	⊢ ( 𝜑 → ¬ 𝐶 ∈ { 0 } )
16	9 15	eldifd	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑆 ∖ { 0 } ) )
17	2	frlmsca	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
18	7 11 17	syl2anc	⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑊 ) )
19	18	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20	4 19	eqtrid	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21	18	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
22	6 21	eqtrid	⊢ ( 𝜑 → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
23	22	sneqd	⊢ ( 𝜑 → { 0 } = { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
24	20 23	difeq12d	⊢ ( 𝜑 → ( 𝑆 ∖ { 0 } ) = ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
25	16 24	eleqtrd	⊢ ( 𝜑 → 𝐶 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
26		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) }
27		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
28		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
29		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
30	26 3 27 5 28 29	prjspvs	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝐶 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐶 · 𝑋 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑋 )
31	13 8 25 30	syl3anc	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑋 )
32	1 2 3 4 5	prjspnerlem	⊢ ( 𝐾 ∈ DivRing → ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
33	7 32	syl	⊢ ( 𝜑 → ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
34	33	breqd	⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) ∼ 𝑋 ↔ ( 𝐶 · 𝑋 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑋 ) )
35	31 34	mpbird	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∼ 𝑋 )