Theorem prjspvs

Description: A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-2023)

	Ref	Expression
Hypotheses	prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspertr.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
	prjspertr.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
	prjspertr.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
	prjspertr.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	prjspreln0.z	⊢ 0 = ( 0g ‘ 𝑆 )
Assertion	prjspvs	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∼ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspertr.b	⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
3		prjspertr.s	⊢ 𝑆 = ( Scalar ‘ 𝑉 )
4		prjspertr.x	⊢ · = ( ·𝑠 ‘ 𝑉 )
5		prjspertr.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		prjspreln0.z	⊢ 0 = ( 0g ‘ 𝑆 )
7		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
8		lveclmod	⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
9	8	3ad2ant1	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑉 ∈ LMod )
10		eldifi	⊢ ( 𝑁 ∈ ( 𝐾 ∖ { 0 } ) → 𝑁 ∈ 𝐾 )
11	10	3ad2ant3	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑁 ∈ 𝐾 )
12		difss	⊢ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ⊆ ( Base ‘ 𝑉 )
13	2 12	eqsstri	⊢ 𝐵 ⊆ ( Base ‘ 𝑉 )
14	13	sseli	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑉 ) )
15	14	3ad2ant2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
16	7 3 4 5 9 11 15	lmodvscld	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∈ ( Base ‘ 𝑉 ) )
17		eldifsni	⊢ ( 𝑁 ∈ ( 𝐾 ∖ { 0 } ) → 𝑁 ≠ 0 )
18	17	3ad2ant3	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑁 ≠ 0 )
19		eldifsni	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
20	19 2	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
21	20	3ad2ant2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
22		eqid	⊢ ( 0g ‘ 𝑉 ) = ( 0g ‘ 𝑉 )
23		simp1	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑉 ∈ LVec )
24	7 4 3 5 6 22 23 11 15	lvecvsn0	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( ( 𝑁 · 𝑋 ) ≠ ( 0g ‘ 𝑉 ) ↔ ( 𝑁 ≠ 0 ∧ 𝑋 ≠ ( 0g ‘ 𝑉 ) ) ) )
25	18 21 24	mpbir2and	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ≠ ( 0g ‘ 𝑉 ) )
26		nelsn	⊢ ( ( 𝑁 · 𝑋 ) ≠ ( 0g ‘ 𝑉 ) → ¬ ( 𝑁 · 𝑋 ) ∈ { ( 0g ‘ 𝑉 ) } )
27	25 26	syl	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ¬ ( 𝑁 · 𝑋 ) ∈ { ( 0g ‘ 𝑉 ) } )
28	16 27	eldifd	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) )
29	28 2	eleqtrrdi	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
30		simp2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑋 ∈ 𝐵 )
31		oveq1	⊢ ( 𝑁 = 𝑚 → ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
32	31	eqcoms	⊢ ( 𝑚 = 𝑁 → ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
33		tbtru	⊢ ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ⊤ ) )
34	32 33	sylib	⊢ ( 𝑚 = 𝑁 → ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ⊤ ) )
35	34	adantl	⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) ∧ 𝑚 = 𝑁 ) → ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ⊤ ) )
36		trud	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ⊤ )
37	11 35 36	rspcedvd	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ∃ 𝑚 ∈ 𝐾 ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
38	1	prjsprel	⊢ ( ( 𝑁 · 𝑋 ) ∼ 𝑋 ↔ ( ( ( 𝑁 · 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ) )
39	29 30 37 38	syl21anbrc	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∼ 𝑋 )