Metamath Proof Explorer

Theorem lspsneu

Description: Nonzero vectors with equal singleton spans have a unique proportionality constant. (Contributed by NM, 31-May-2015)

Ref Expression
Hypotheses lspsneu.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsneu.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
lspsneu.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
lspsneu.o ⊢ 𝑂 = ( 0g ‘ 𝑆 )
lspsneu.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lspsneu.z ⊢ 0 = ( 0g ‘ 𝑊 )
lspsneu.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsneu.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspsneu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsneu.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion lspsneu ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃! 𝑘 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑘 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lspsneu.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsneu.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
3 lspsneu.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 lspsneu.o ⊢ 𝑂 = ( 0g ‘ 𝑆 )
5 lspsneu.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lspsneu.z ⊢ 0 = ( 0g ‘ 𝑊 )
7 lspsneu.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
8 lspsneu.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
9 lspsneu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lspsneu.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
11 10 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
12 1 2 3 4 5 7 8 9 11 lspsneq ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
13 12 biimpd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
14 eqtr2 ⊢ ( ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) → ( 𝑗 · 𝑌 ) = ( 𝑖 · 𝑌 ) )
15 14 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → ( 𝑗 · 𝑌 ) = ( 𝑖 · 𝑌 ) )
16 simp1l ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝜑 )
17 16 8 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑊 ∈ LVec )
18 simp2l ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) )
19 18 eldifad ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑗 ∈ 𝐾 )
20 simp2r ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) )
21 20 eldifad ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑖 ∈ 𝐾 )
22 16 11 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑌 ∈ 𝑉 )
23 eldifsni ⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) → 𝑌 ≠ 0 )
24 16 10 23 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑌 ≠ 0 )
25 1 5 2 3 6 17 19 21 22 24 lvecvscan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → ( ( 𝑗 · 𝑌 ) = ( 𝑖 · 𝑌 ) ↔ 𝑗 = 𝑖 ) )
26 15 25 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) ∧ ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) ) → 𝑗 = 𝑖 )
27 26 3exp ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) → ( ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) → ( ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) → 𝑗 = 𝑖 ) ) )
28 27 ex ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( ( 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∧ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ) → ( ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) → 𝑗 = 𝑖 ) ) ) )
29 28 ralrimdvv ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ∀ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∀ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ( ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) → 𝑗 = 𝑖 ) ) )
30 13 29 jcad ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( ∃ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ∧ ∀ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∀ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ( ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) → 𝑗 = 𝑖 ) ) ) )
31 oveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 · 𝑌 ) = ( 𝑖 · 𝑌 ) )
32 31 eqeq2d ⊢ ( 𝑗 = 𝑖 → ( 𝑋 = ( 𝑗 · 𝑌 ) ↔ 𝑋 = ( 𝑖 · 𝑌 ) ) )
33 32 reu4 ⊢ ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ↔ ( ∃ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ∧ ∀ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) ∀ 𝑖 ∈ ( 𝐾 ∖ { 𝑂 } ) ( ( 𝑋 = ( 𝑗 · 𝑌 ) ∧ 𝑋 = ( 𝑖 · 𝑌 ) ) → 𝑗 = 𝑖 ) ) )
34 30 33 syl6ibr ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
35 reurex ⊢ ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) )
36 35 12 syl5ibr ⊢ ( 𝜑 → ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
37 34 36 impbid ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
38 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 · 𝑌 ) = ( 𝑘 · 𝑌 ) )
39 38 eqeq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑋 = ( 𝑗 · 𝑌 ) ↔ 𝑋 = ( 𝑘 · 𝑌 ) ) )
40 39 cbvreuvw ⊢ ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ↔ ∃! 𝑘 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑘 · 𝑌 ) )
41 37 40 bitrdi ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃! 𝑘 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑘 · 𝑌 ) ) )