Metamath Proof Explorer

Theorem lspsneq

Description: Equal spans of singletons must have proportional vectors. See lspsnss2 for comparable span version. TODO: can proof be shortened? (Contributed by NM, 21-Mar-2015)

Ref Expression
Hypotheses lspsneq.v 
|- V = ( Base ` W )
lspsneq.s 
|- S = ( Scalar ` W )
lspsneq.k 
|- K = ( Base ` S )
lspsneq.o 
|- .0. = ( 0g ` S )
lspsneq.t 
|- .x. = ( .s ` W )
lspsneq.n 
|- N = ( LSpan ` W )
lspsneq.w 
|- ( ph -> W e. LVec )
lspsneq.x 
|- ( ph -> X e. V )
lspsneq.y 
|- ( ph -> Y e. V )
Assertion lspsneq 
|- ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E. k e. ( K \ { .0. } ) X = ( k .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 lspsneq.v 
 |-  V = ( Base ` W )
2 lspsneq.s 
 |-  S = ( Scalar ` W )
3 lspsneq.k 
 |-  K = ( Base ` S )
4 lspsneq.o 
 |-  .0. = ( 0g ` S )
5 lspsneq.t 
 |-  .x. = ( .s ` W )
6 lspsneq.n 
 |-  N = ( LSpan ` W )
7 lspsneq.w 
 |-  ( ph -> W e. LVec )
8 lspsneq.x 
 |-  ( ph -> X e. V )
9 lspsneq.y 
 |-  ( ph -> Y e. V )
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 7 10 syl 
 |-  ( ph -> W e. LMod )
12 2 lmodring 
 |-  ( W e. LMod -> S e. Ring )
13 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
14 3 13 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. K )
15 11 12 14 3syl 
 |-  ( ph -> ( 1r ` S ) e. K )
16 2 lvecdrng 
 |-  ( W e. LVec -> S e. DivRing )
17 4 13 drngunz 
 |-  ( S e. DivRing -> ( 1r ` S ) =/= .0. )
18 7 16 17 3syl 
 |-  ( ph -> ( 1r ` S ) =/= .0. )
19 eldifsn 
 |-  ( ( 1r ` S ) e. ( K \ { .0. } ) <-> ( ( 1r ` S ) e. K /\ ( 1r ` S ) =/= .0. ) )
20 15 18 19 sylanbrc 
 |-  ( ph -> ( 1r ` S ) e. ( K \ { .0. } ) )
21 20 ad2antrr 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y = ( 0g ` W ) ) -> ( 1r ` S ) e. ( K \ { .0. } ) )
22 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
23 1 22 lmod0vcl 
 |-  ( W e. LMod -> ( 0g ` W ) e. V )
24 1 2 5 13 lmodvs1 
 |-  ( ( W e. LMod /\ ( 0g ` W ) e. V ) -> ( ( 1r ` S ) .x. ( 0g ` W ) ) = ( 0g ` W ) )
25 11 23 24 syl2anc2 
 |-  ( ph -> ( ( 1r ` S ) .x. ( 0g ` W ) ) = ( 0g ` W ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y = ( 0g ` W ) ) -> ( ( 1r ` S ) .x. ( 0g ` W ) ) = ( 0g ` W ) )
27 oveq2 
 |-  ( Y = ( 0g ` W ) -> ( ( 1r ` S ) .x. Y ) = ( ( 1r ` S ) .x. ( 0g ` W ) ) )
28 27 adantl 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y = ( 0g ` W ) ) -> ( ( 1r ` S ) .x. Y ) = ( ( 1r ` S ) .x. ( 0g ` W ) ) )
29 11 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> W e. LMod )
30 8 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> X e. V )
31 9 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> Y e. V )
32 simpr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( N ` { X } ) = ( N ` { Y } ) )
33 1 22 6 29 30 31 32 lspsneq0b 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( X = ( 0g ` W ) <-> Y = ( 0g ` W ) ) )
34 33 biimpar 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y = ( 0g ` W ) ) -> X = ( 0g ` W ) )
35 26 28 34 3eqtr4rd 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y = ( 0g ` W ) ) -> X = ( ( 1r ` S ) .x. Y ) )
36 oveq1 
 |-  ( j = ( 1r ` S ) -> ( j .x. Y ) = ( ( 1r ` S ) .x. Y ) )
37 36 rspceeqv 
 |-  ( ( ( 1r ` S ) e. ( K \ { .0. } ) /\ X = ( ( 1r ` S ) .x. Y ) ) -> E. j e. ( K \ { .0. } ) X = ( j .x. Y ) )
38 21 35 37 syl2anc 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y = ( 0g ` W ) ) -> E. j e. ( K \ { .0. } ) X = ( j .x. Y ) )
39 eqimss 
 |-  ( ( N ` { X } ) = ( N ` { Y } ) -> ( N ` { X } ) C_ ( N ` { Y } ) )
40 39 adantl 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( N ` { X } ) C_ ( N ` { Y } ) )
41 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
42 1 41 6 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
43 11 9 42 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
44 43 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
45 1 41 6 29 44 30 ellspsn5b 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( X e. ( N ` { Y } ) <-> ( N ` { X } ) C_ ( N ` { Y } ) ) )
46 40 45 mpbird 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> X e. ( N ` { Y } ) )
47 2 3 1 5 6 ellspsn 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( X e. ( N ` { Y } ) <-> E. j e. K X = ( j .x. Y ) ) )
48 29 31 47 syl2anc 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( X e. ( N ` { Y } ) <-> E. j e. K X = ( j .x. Y ) ) )
49 46 48 mpbid 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> E. j e. K X = ( j .x. Y ) )
50 49 adantr 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) -> E. j e. K X = ( j .x. Y ) )
51 simprl 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> j e. K )
52 simpr 
 |-  ( ( j e. K /\ X = ( j .x. Y ) ) -> X = ( j .x. Y ) )
53 52 adantl 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> X = ( j .x. Y ) )
54 33 biimpd 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( X = ( 0g ` W ) -> Y = ( 0g ` W ) ) )
55 54 necon3d 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> ( Y =/= ( 0g ` W ) -> X =/= ( 0g ` W ) ) )
56 55 imp 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) -> X =/= ( 0g ` W ) )
57 56 adantr 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> X =/= ( 0g ` W ) )
58 53 57 eqnetrrd 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> ( j .x. Y ) =/= ( 0g ` W ) )
59 7 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> W e. LVec )
60 59 ad2antrr 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> W e. LVec )
61 31 ad2antrr 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> Y e. V )
62 1 5 2 3 4 22 60 51 61 lvecvsn0 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> ( ( j .x. Y ) =/= ( 0g ` W ) <-> ( j =/= .0. /\ Y =/= ( 0g ` W ) ) ) )
63 58 62 mpbid 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> ( j =/= .0. /\ Y =/= ( 0g ` W ) ) )
64 63 simpld 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> j =/= .0. )
65 eldifsn 
 |-  ( j e. ( K \ { .0. } ) <-> ( j e. K /\ j =/= .0. ) )
66 51 64 65 sylanbrc 
 |-  ( ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) /\ ( j e. K /\ X = ( j .x. Y ) ) ) -> j e. ( K \ { .0. } ) )
67 50 66 53 reximssdv 
 |-  ( ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) /\ Y =/= ( 0g ` W ) ) -> E. j e. ( K \ { .0. } ) X = ( j .x. Y ) )
68 38 67 pm2.61dane 
 |-  ( ( ph /\ ( N ` { X } ) = ( N ` { Y } ) ) -> E. j e. ( K \ { .0. } ) X = ( j .x. Y ) )
69 68 ex 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> E. j e. ( K \ { .0. } ) X = ( j .x. Y ) ) )
70 7 adantr 
 |-  ( ( ph /\ j e. ( K \ { .0. } ) ) -> W e. LVec )
71 eldifi 
 |-  ( j e. ( K \ { .0. } ) -> j e. K )
72 71 adantl 
 |-  ( ( ph /\ j e. ( K \ { .0. } ) ) -> j e. K )
73 eldifsni 
 |-  ( j e. ( K \ { .0. } ) -> j =/= .0. )
74 73 adantl 
 |-  ( ( ph /\ j e. ( K \ { .0. } ) ) -> j =/= .0. )
75 9 adantr 
 |-  ( ( ph /\ j e. ( K \ { .0. } ) ) -> Y e. V )
76 1 2 5 3 4 6 lspsnvs 
 |-  ( ( W e. LVec /\ ( j e. K /\ j =/= .0. ) /\ Y e. V ) -> ( N ` { ( j .x. Y ) } ) = ( N ` { Y } ) )
77 70 72 74 75 76 syl121anc 
 |-  ( ( ph /\ j e. ( K \ { .0. } ) ) -> ( N ` { ( j .x. Y ) } ) = ( N ` { Y } ) )
78 77 ex 
 |-  ( ph -> ( j e. ( K \ { .0. } ) -> ( N ` { ( j .x. Y ) } ) = ( N ` { Y } ) ) )
79 sneq 
 |-  ( X = ( j .x. Y ) -> { X } = { ( j .x. Y ) } )
80 79 fveqeq2d 
 |-  ( X = ( j .x. Y ) -> ( ( N ` { X } ) = ( N ` { Y } ) <-> ( N ` { ( j .x. Y ) } ) = ( N ` { Y } ) ) )
81 80 biimprcd 
 |-  ( ( N ` { ( j .x. Y ) } ) = ( N ` { Y } ) -> ( X = ( j .x. Y ) -> ( N ` { X } ) = ( N ` { Y } ) ) )
82 78 81 syl6 
 |-  ( ph -> ( j e. ( K \ { .0. } ) -> ( X = ( j .x. Y ) -> ( N ` { X } ) = ( N ` { Y } ) ) ) )
83 82 rexlimdv 
 |-  ( ph -> ( E. j e. ( K \ { .0. } ) X = ( j .x. Y ) -> ( N ` { X } ) = ( N ` { Y } ) ) )
84 69 83 impbid 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E. j e. ( K \ { .0. } ) X = ( j .x. Y ) ) )
85 oveq1 
 |-  ( j = k -> ( j .x. Y ) = ( k .x. Y ) )
86 85 eqeq2d 
 |-  ( j = k -> ( X = ( j .x. Y ) <-> X = ( k .x. Y ) ) )
87 86 cbvrexvw 
 |-  ( E. j e. ( K \ { .0. } ) X = ( j .x. Y ) <-> E. k e. ( K \ { .0. } ) X = ( k .x. Y ) )
88 84 87 bitrdi 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E. k e. ( K \ { .0. } ) X = ( k .x. Y ) ) )