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	imbitrrdi	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
35		reurex	⊢ ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) → ∃ 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) )
36	35 12	imbitrrid	⊢ ( 𝜑 → ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
37	34 36	impbid	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ) )
38		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 · 𝑌 ) = ( 𝑘 · 𝑌 ) )
39	38	eqeq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑋 = ( 𝑗 · 𝑌 ) ↔ 𝑋 = ( 𝑘 · 𝑌 ) ) )
40	39	cbvreuvw	⊢ ( ∃! 𝑗 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑗 · 𝑌 ) ↔ ∃! 𝑘 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑘 · 𝑌 ) )
41	37 40	bitrdi	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ↔ ∃! 𝑘 ∈ ( 𝐾 ∖ { 𝑂 } ) 𝑋 = ( 𝑘 · 𝑌 ) ) )