Metamath Proof Explorer

Theorem prjspreln0

Description: Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023)

Ref Expression
Hypotheses prjsprel.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐾 𝑥 = ( 𝑙 · 𝑦 ) ) }
prjspertr.b ⊢ 𝐵 = ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } )
prjspertr.s ⊢ 𝑆 = ( Scalar ‘ 𝑉 )
prjspertr.x ⊢ · = ( ·𝑠 ‘ 𝑉 )
prjspertr.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
prjspreln0.z ⊢ 0 = ( 0g ‘ 𝑆 )
Assertion prjspreln0 ( 𝑉 ∈ 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 1 prjsprel ⊢ ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )
8 simprl ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑚 ∈ 𝐾 )
9 simplrl ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑋 ∈ 𝐵 )
10 eldifsni ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
11 10 2 eleq2s ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
12 9 11 syl ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑋 ≠ ( 0g ‘ 𝑉 ) )
13 simplrr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → 𝑋 = ( 𝑚 · 𝑌 ) )
14 simpr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → 𝑚 = 0 )
15 14 oveq1d ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → ( 𝑚 · 𝑌 ) = ( 0 · 𝑌 ) )
16 lveclmod ⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
17 16 ad3antrrr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → 𝑉 ∈ LMod )
18 difss ⊢ ( ( Base ‘ 𝑉 ) ∖ { ( 0g ‘ 𝑉 ) } ) ⊆ ( Base ‘ 𝑉 )
19 2 18 eqsstri ⊢ 𝐵 ⊆ ( Base ‘ 𝑉 )
20 simplrr ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ∧ 𝑚 = 0 ) ) → 𝑌 ∈ 𝐵 )
21 20 anassrs ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → 𝑌 ∈ 𝐵 )
22 19 21 sselid ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → 𝑌 ∈ ( Base ‘ 𝑉 ) )
23 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
24 eqid ⊢ ( 0g ‘ 𝑉 ) = ( 0g ‘ 𝑉 )
25 23 3 4 6 24 lmod0vs ⊢ ( ( 𝑉 ∈ LMod ∧ 𝑌 ∈ ( Base ‘ 𝑉 ) ) → ( 0 · 𝑌 ) = ( 0g ‘ 𝑉 ) )
26 17 22 25 syl2anc ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → ( 0 · 𝑌 ) = ( 0g ‘ 𝑉 ) )
27 13 15 26 3eqtrd ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) ∧ 𝑚 = 0 ) → 𝑋 = ( 0g ‘ 𝑉 ) )
28 12 27 mteqand ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑚 ≠ 0 )
29 nelsn ⊢ ( 𝑚 ≠ 0 → ¬ 𝑚 ∈ { 0 } )
30 28 29 syl ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ¬ 𝑚 ∈ { 0 } )
31 8 30 eldifd ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑚 ∈ ( 𝐾 ∖ { 0 } ) )
32 31 ex ⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑚 ∈ ( 𝐾 ∖ { 0 } ) ) )
33 simpr ⊢ ( ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → 𝑋 = ( 𝑚 · 𝑌 ) )
34 32 33 jca2 ⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑚 ∈ 𝐾 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ( 𝑚 ∈ ( 𝐾 ∖ { 0 } ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
35 34 reximdv2 ⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) → ∃ 𝑚 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑚 · 𝑌 ) ) )
36 difss ⊢ ( 𝐾 ∖ { 0 } ) ⊆ 𝐾
37 ssrexv ⊢ ( ( 𝐾 ∖ { 0 } ) ⊆ 𝐾 → ( ∃ 𝑚 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑚 · 𝑌 ) → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )
38 36 37 mp1i ⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑚 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑚 · 𝑌 ) → ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) )
39 35 38 impbid ⊢ ( ( 𝑉 ∈ LVec ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ↔ ∃ 𝑚 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑚 · 𝑌 ) ) )
40 39 pm5.32da ⊢ ( 𝑉 ∈ LVec → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝐾 𝑋 = ( 𝑚 · 𝑌 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
41 7 40 syl5bb ⊢ ( 𝑉 ∈ LVec → ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( 𝐾 ∖ { 0 } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )