This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspdisjb

Description: A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 lspdisjb.v 
 |-  V = ( Base ` W )
2 lspdisjb.o 
 |-  .0. = ( 0g ` W )
3 lspdisjb.n 
 |-  N = ( LSpan ` W )
4 lspdisjb.s 
 |-  S = ( LSubSp ` W )
5 lspdisjb.w 
 |-  ( ph -> W e. LVec )
6 lspdisjb.u 
 |-  ( ph -> U e. S )
7 lspdisjb.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
8 5 adantr 
 |-  ( ( ph /\ -. X e. U ) -> W e. LVec )
9 6 adantr 
 |-  ( ( ph /\ -. X e. U ) -> U e. S )
10 7 eldifad 
 |-  ( ph -> X e. V )
11 10 adantr 
 |-  ( ( ph /\ -. X e. U ) -> X e. V )
12 simpr 
 |-  ( ( ph /\ -. X e. U ) -> -. X e. U )
13 1 2 3 4 8 9 11 12 lspdisj 
 |-  ( ( ph /\ -. X e. U ) -> ( ( N ` { X } ) i^i U ) = { .0. } )
14 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
15 7 14 syl 
 |-  ( ph -> X =/= .0. )
16 15 adantr 
 |-  ( ( ph /\ ( ( N ` { X } ) i^i U ) = { .0. } ) -> X =/= .0. )
17 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
18 5 17 syl 
 |-  ( ph -> W e. LMod )
19 1 3 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
20 18 10 19 syl2anc 
 |-  ( ph -> X e. ( N ` { X } ) )
21 elin 
 |-  ( X e. ( ( N ` { X } ) i^i U ) <-> ( X e. ( N ` { X } ) /\ X e. U ) )
22 eleq2 
 |-  ( ( ( N ` { X } ) i^i U ) = { .0. } -> ( X e. ( ( N ` { X } ) i^i U ) <-> X e. { .0. } ) )
23 elsni 
 |-  ( X e. { .0. } -> X = .0. )
24 22 23 biimtrdi 
 |-  ( ( ( N ` { X } ) i^i U ) = { .0. } -> ( X e. ( ( N ` { X } ) i^i U ) -> X = .0. ) )
25 21 24 biimtrrid 
 |-  ( ( ( N ` { X } ) i^i U ) = { .0. } -> ( ( X e. ( N ` { X } ) /\ X e. U ) -> X = .0. ) )
26 25 expd 
 |-  ( ( ( N ` { X } ) i^i U ) = { .0. } -> ( X e. ( N ` { X } ) -> ( X e. U -> X = .0. ) ) )
27 20 26 mpan9 
 |-  ( ( ph /\ ( ( N ` { X } ) i^i U ) = { .0. } ) -> ( X e. U -> X = .0. ) )
28 27 necon3ad 
 |-  ( ( ph /\ ( ( N ` { X } ) i^i U ) = { .0. } ) -> ( X =/= .0. -> -. X e. U ) )
29 16 28 mpd 
 |-  ( ( ph /\ ( ( N ` { X } ) i^i U ) = { .0. } ) -> -. X e. U )
30 13 29 impbida 
 |-  ( ph -> ( -. X e. U <-> ( ( N ` { X } ) i^i U ) = { .0. } ) )