Metamath Proof Explorer


Theorem lspdisj

Description: The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015)

Ref Expression
Hypotheses lspdisj.v
|- V = ( Base ` W )
lspdisj.o
|- .0. = ( 0g ` W )
lspdisj.n
|- N = ( LSpan ` W )
lspdisj.s
|- S = ( LSubSp ` W )
lspdisj.w
|- ( ph -> W e. LVec )
lspdisj.u
|- ( ph -> U e. S )
lspdisj.x
|- ( ph -> X e. V )
lspdisj.e
|- ( ph -> -. X e. U )
Assertion lspdisj
|- ( ph -> ( ( N ` { X } ) i^i U ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lspdisj.v
 |-  V = ( Base ` W )
2 lspdisj.o
 |-  .0. = ( 0g ` W )
3 lspdisj.n
 |-  N = ( LSpan ` W )
4 lspdisj.s
 |-  S = ( LSubSp ` W )
5 lspdisj.w
 |-  ( ph -> W e. LVec )
6 lspdisj.u
 |-  ( ph -> U e. S )
7 lspdisj.x
 |-  ( ph -> X e. V )
8 lspdisj.e
 |-  ( ph -> -. X e. U )
9 lveclmod
 |-  ( W e. LVec -> W e. LMod )
10 5 9 syl
 |-  ( ph -> W e. LMod )
11 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 eqid
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
13 eqid
 |-  ( .s ` W ) = ( .s ` W )
14 11 12 1 13 3 lspsnel
 |-  ( ( W e. LMod /\ X e. V ) -> ( v e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) )
15 10 7 14 syl2anc
 |-  ( ph -> ( v e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) )
16 15 biimpa
 |-  ( ( ph /\ v e. ( N ` { X } ) ) -> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) )
17 16 adantrr
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) )
18 simprr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> v = ( k ( .s ` W ) X ) )
19 8 ad2antrr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> -. X e. U )
20 simplr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> v e. U )
21 18 20 eqeltrrd
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( k ( .s ` W ) X ) e. U )
22 eqid
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
23 5 ad2antrr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> W e. LVec )
24 6 ad2antrr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> U e. S )
25 7 ad2antrr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> X e. V )
26 simprl
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
27 1 13 11 12 22 4 23 24 25 26 lssvs0or
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( ( k ( .s ` W ) X ) e. U <-> ( k = ( 0g ` ( Scalar ` W ) ) \/ X e. U ) ) )
28 21 27 mpbid
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) \/ X e. U ) )
29 28 orcomd
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( X e. U \/ k = ( 0g ` ( Scalar ` W ) ) ) )
30 29 ord
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( -. X e. U -> k = ( 0g ` ( Scalar ` W ) ) ) )
31 19 30 mpd
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> k = ( 0g ` ( Scalar ` W ) ) )
32 31 oveq1d
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( k ( .s ` W ) X ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) )
33 10 ad2antrr
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> W e. LMod )
34 1 11 13 22 2 lmod0vs
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. )
35 33 25 34 syl2anc
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. )
36 18 32 35 3eqtrd
 |-  ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> v = .0. )
37 36 exp32
 |-  ( ( ph /\ v e. U ) -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v = ( k ( .s ` W ) X ) -> v = .0. ) ) )
38 37 adantrl
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v = ( k ( .s ` W ) X ) -> v = .0. ) ) )
39 38 rexlimdv
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> ( E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) -> v = .0. ) )
40 17 39 mpd
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> v = .0. )
41 40 ex
 |-  ( ph -> ( ( v e. ( N ` { X } ) /\ v e. U ) -> v = .0. ) )
42 elin
 |-  ( v e. ( ( N ` { X } ) i^i U ) <-> ( v e. ( N ` { X } ) /\ v e. U ) )
43 velsn
 |-  ( v e. { .0. } <-> v = .0. )
44 41 42 43 3imtr4g
 |-  ( ph -> ( v e. ( ( N ` { X } ) i^i U ) -> v e. { .0. } ) )
45 44 ssrdv
 |-  ( ph -> ( ( N ` { X } ) i^i U ) C_ { .0. } )
46 1 4 3 lspsncl
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S )
47 10 7 46 syl2anc
 |-  ( ph -> ( N ` { X } ) e. S )
48 2 4 lss0ss
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. S ) -> { .0. } C_ ( N ` { X } ) )
49 10 47 48 syl2anc
 |-  ( ph -> { .0. } C_ ( N ` { X } ) )
50 2 4 lss0ss
 |-  ( ( W e. LMod /\ U e. S ) -> { .0. } C_ U )
51 10 6 50 syl2anc
 |-  ( ph -> { .0. } C_ U )
52 49 51 ssind
 |-  ( ph -> { .0. } C_ ( ( N ` { X } ) i^i U ) )
53 45 52 eqssd
 |-  ( ph -> ( ( N ` { X } ) i^i U ) = { .0. } )