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		lveclmod	⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
8	7	3ad2ant1	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑉 ∈ LMod )
9		eldifi	⊢ ( 𝑁 ∈ ( 𝐾 ∖ { 0 } ) → 𝑁 ∈ 𝐾 )
10	9	3ad2ant3	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑁 ∈ 𝐾 )
11		difss	⊢ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ⊆ ( Base ‘ 𝑉 )
12	2 11	eqsstri	⊢ 𝐵 ⊆ ( Base ‘ 𝑉 )
13	12	sseli	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑉 ) )
14	13	3ad2ant2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑋 ∈ ( Base ‘ 𝑉 ) )
15		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
16	15 3 4 5	lmodvscl	⊢ ( ( 𝑉 ∈ LMod ∧ 𝑁 ∈ 𝐾 ∧ 𝑋 ∈ ( Base ‘ 𝑉 ) ) → ( 𝑁 · 𝑋 ) ∈ ( Base ‘ 𝑉 ) )
17	8 10 14 16	syl3anc	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∈ ( Base ‘ 𝑉 ) )
18		eldifsni	⊢ ( 𝑁 ∈ ( 𝐾 ∖ { 0 } ) → 𝑁 ≠ 0 )
19	18	3ad2ant3	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑁 ≠ 0 )
20		eldifsni	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
21	20 2	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
22	21	3ad2ant2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
23		eqid	⊢ ( 0g ‘ 𝑉 ) = ( 0g ‘ 𝑉 )
24		simp1	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑉 ∈ LVec )
25	15 4 3 5 6 23 24 10 14	lvecvsn0	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( ( 𝑁 · 𝑋 ) ≠ ( 0g ‘ 𝑉 ) ↔ ( 𝑁 ≠ 0 ∧ 𝑋 ≠ ( 0g ‘ 𝑉 ) ) ) )
26	19 22 25	mpbir2and	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ≠ ( 0g ‘ 𝑉 ) )
27		nelsn	⊢ ( ( 𝑁 · 𝑋 ) ≠ ( 0g ‘ 𝑉 ) → ¬ ( 𝑁 · 𝑋 ) ∈ { ( 0g ‘ 𝑉 ) } )
28	26 27	syl	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ¬ ( 𝑁 · 𝑋 ) ∈ { ( 0g ‘ 𝑉 ) } )
29	17 28	eldifd	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) )
30	29 2	eleqtrrdi	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
31		simp2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → 𝑋 ∈ 𝐵 )
32		oveq1	⊢ ( 𝑁 = 𝑚 → ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
33	32	eqcoms	⊢ ( 𝑚 = 𝑁 → ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
34		tbtru	⊢ ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ⊤ ) )
35	33 34	sylib	⊢ ( 𝑚 = 𝑁 → ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ⊤ ) )
36	35	adantl	⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) ∧ 𝑚 = 𝑁 ) → ( ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ↔ ⊤ ) )
37		trud	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ⊤ )
38	10 36 37	rspcedvd	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ∃ 𝑚 ∈ 𝐾 ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
39	1	prjsprel	⊢ ( ( 𝑁 · 𝑋 ) ∼ 𝑋 ↔ ( ( ( 𝑁 · 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 ( 𝑁 · 𝑋 ) = ( 𝑚 · 𝑋 ) ) )
40	30 31 38 39	syl21anbrc	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ( 𝐾 ∖ { 0 } ) ) → ( 𝑁 · 𝑋 ) ∼ 𝑋 )