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. } )