Metamath Proof Explorer


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 } ) ) → ( 𝑁 · 𝑋 ) 𝑋 )