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 V = Base W
lspsneu.s S = Scalar W
lspsneu.k K = Base S
lspsneu.o O = 0 S
lspsneu.t · ˙ = W
lspsneu.z 0 ˙ = 0 W
lspsneu.n N = LSpan W
lspsneu.w φ W LVec
lspsneu.x φ X V
lspsneu.y φ Y V 0 ˙
Assertion lspsneu φ N X = N Y ∃! k K O X = k · ˙ Y

Proof

Step Hyp Ref Expression
1 lspsneu.v V = Base W
2 lspsneu.s S = Scalar W
3 lspsneu.k K = Base S
4 lspsneu.o O = 0 S
5 lspsneu.t · ˙ = W
6 lspsneu.z 0 ˙ = 0 W
7 lspsneu.n N = LSpan W
8 lspsneu.w φ W LVec
9 lspsneu.x φ X V
10 lspsneu.y φ Y V 0 ˙
11 10 eldifad φ Y V
12 1 2 3 4 5 7 8 9 11 lspsneq φ N X = N Y j K O X = j · ˙ Y
13 12 biimpd φ N X = N Y j K O X = j · ˙ Y
14 eqtr2 X = j · ˙ Y X = i · ˙ Y j · ˙ Y = i · ˙ Y
15 14 3ad2ant3 φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j · ˙ Y = i · ˙ Y
16 simp1l φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y φ
17 16 8 syl φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y W LVec
18 simp2l φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j K O
19 18 eldifad φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j K
20 simp2r φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y i K O
21 20 eldifad φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y i K
22 16 11 syl φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y Y V
23 eldifsni Y V 0 ˙ Y 0 ˙
24 16 10 23 3syl φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y Y 0 ˙
25 1 5 2 3 6 17 19 21 22 24 lvecvscan2 φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j · ˙ Y = i · ˙ Y j = i
26 15 25 mpbid φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j = i
27 26 3exp φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j = i
28 27 ex φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j = i
29 28 ralrimdvv φ N X = N Y j K O i K O X = j · ˙ Y X = i · ˙ Y j = i
30 13 29 jcad φ N X = N Y j K O X = j · ˙ Y j K O i K O X = j · ˙ Y X = i · ˙ Y j = i
31 oveq1 j = i j · ˙ Y = i · ˙ Y
32 31 eqeq2d j = i X = j · ˙ Y X = i · ˙ Y
33 32 reu4 ∃! j K O X = j · ˙ Y j K O X = j · ˙ Y j K O i K O X = j · ˙ Y X = i · ˙ Y j = i
34 30 33 syl6ibr φ N X = N Y ∃! j K O X = j · ˙ Y
35 reurex ∃! j K O X = j · ˙ Y j K O X = j · ˙ Y
36 35 12 syl5ibr φ ∃! j K O X = j · ˙ Y N X = N Y
37 34 36 impbid φ N X = N Y ∃! j K O X = j · ˙ Y
38 oveq1 j = k j · ˙ Y = k · ˙ Y
39 38 eqeq2d j = k X = j · ˙ Y X = k · ˙ Y
40 39 cbvreuvw ∃! j K O X = j · ˙ Y ∃! k K O X = k · ˙ Y
41 37 40 bitrdi φ N X = N Y ∃! k K O X = k · ˙ Y