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 = ( 0g ` S )
lspsneu.t 
|- .x. = ( .s ` W )
lspsneu.z 
|- .0. = ( 0g ` W )
lspsneu.n 
|- N = ( LSpan ` W )
lspsneu.w 
|- ( ph -> W e. LVec )
lspsneu.x 
|- ( ph -> X e. V )
lspsneu.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
Assertion lspsneu 
|- ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E! k e. ( K \ { O } ) X = ( k .x. 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 = ( 0g ` S )
5 lspsneu.t 
 |-  .x. = ( .s ` W )
6 lspsneu.z 
 |-  .0. = ( 0g ` W )
7 lspsneu.n 
 |-  N = ( LSpan ` W )
8 lspsneu.w 
 |-  ( ph -> W e. LVec )
9 lspsneu.x 
 |-  ( ph -> X e. V )
10 lspsneu.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
11 10 eldifad 
 |-  ( ph -> Y e. V )
12 1 2 3 4 5 7 8 9 11 lspsneq 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E. j e. ( K \ { O } ) X = ( j .x. Y ) ) )
13 12 biimpd 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> E. j e. ( K \ { O } ) X = ( j .x. Y ) ) )
14 eqtr2 
 |-  ( ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) -> ( j .x. Y ) = ( i .x. Y ) )
15 14 3ad2ant3 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> ( j .x. Y ) = ( i .x. Y ) )
16 simp1l 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> ph )
17 16 8 syl 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> W e. LVec )
18 simp2l 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> j e. ( K \ { O } ) )
19 18 eldifad 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> j e. K )
20 simp2r 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> i e. ( K \ { O } ) )
21 20 eldifad 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> i e. K )
22 16 11 syl 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> Y e. V )
23 eldifsni 
 |-  ( Y e. ( V \ { .0. } ) -> Y =/= .0. )
24 16 10 23 3syl 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> Y =/= .0. )
25 1 5 2 3 6 17 19 21 22 24 lvecvscan2 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> ( ( j .x. Y ) = ( i .x. Y ) <-> j = i ) )
26 15 25 mpbid 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) /\ ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) ) -> j = i )
27 26 3exp 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) -> ( ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) -> j = i ) ) )
28 27 ex 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> ( ( j e. ( K \ { O } ) /\ i e. ( K \ { O } ) ) -> ( ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) -> j = i ) ) ) )
29 28 ralrimdvv 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> A. j e. ( K \ { O } ) A. i e. ( K \ { O } ) ( ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) -> j = i ) ) )
30 13 29 jcad 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> ( E. j e. ( K \ { O } ) X = ( j .x. Y ) /\ A. j e. ( K \ { O } ) A. i e. ( K \ { O } ) ( ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) -> j = i ) ) ) )
31 oveq1 
 |-  ( j = i -> ( j .x. Y ) = ( i .x. Y ) )
32 31 eqeq2d 
 |-  ( j = i -> ( X = ( j .x. Y ) <-> X = ( i .x. Y ) ) )
33 32 reu4 
 |-  ( E! j e. ( K \ { O } ) X = ( j .x. Y ) <-> ( E. j e. ( K \ { O } ) X = ( j .x. Y ) /\ A. j e. ( K \ { O } ) A. i e. ( K \ { O } ) ( ( X = ( j .x. Y ) /\ X = ( i .x. Y ) ) -> j = i ) ) )
34 30 33 imbitrrdi 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> E! j e. ( K \ { O } ) X = ( j .x. Y ) ) )
35 reurex 
 |-  ( E! j e. ( K \ { O } ) X = ( j .x. Y ) -> E. j e. ( K \ { O } ) X = ( j .x. Y ) )
36 35 12 imbitrrid 
 |-  ( ph -> ( E! j e. ( K \ { O } ) X = ( j .x. Y ) -> ( N ` { X } ) = ( N ` { Y } ) ) )
37 34 36 impbid 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E! j e. ( K \ { O } ) X = ( j .x. Y ) ) )
38 oveq1 
 |-  ( j = k -> ( j .x. Y ) = ( k .x. Y ) )
39 38 eqeq2d 
 |-  ( j = k -> ( X = ( j .x. Y ) <-> X = ( k .x. Y ) ) )
40 39 cbvreuvw 
 |-  ( E! j e. ( K \ { O } ) X = ( j .x. Y ) <-> E! k e. ( K \ { O } ) X = ( k .x. Y ) )
41 37 40 bitrdi 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E! k e. ( K \ { O } ) X = ( k .x. Y ) ) )