Metamath Proof Explorer

Theorem lspdisj2

Description: Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses lspdisj2.v 
|- V = ( Base ` W )
lspdisj2.o 
|- .0. = ( 0g ` W )
lspdisj2.n 
|- N = ( LSpan ` W )
lspdisj2.w 
|- ( ph -> W e. LVec )
lspdisj2.x 
|- ( ph -> X e. V )
lspdisj2.y 
|- ( ph -> Y e. V )
lspdisj2.q 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion lspdisj2 
|- ( ph -> ( ( N ` { X } ) i^i ( N ` { Y } ) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lspdisj2.v 
 |-  V = ( Base ` W )
2 lspdisj2.o 
 |-  .0. = ( 0g ` W )
3 lspdisj2.n 
 |-  N = ( LSpan ` W )
4 lspdisj2.w 
 |-  ( ph -> W e. LVec )
5 lspdisj2.x 
 |-  ( ph -> X e. V )
6 lspdisj2.y 
 |-  ( ph -> Y e. V )
7 lspdisj2.q 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
8 sneq 
 |-  ( X = .0. -> { X } = { .0. } )
9 8 fveq2d 
 |-  ( X = .0. -> ( N ` { X } ) = ( N ` { .0. } ) )
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 4 10 syl 
 |-  ( ph -> W e. LMod )
12 2 3 lspsn0 
 |-  ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
13 11 12 syl 
 |-  ( ph -> ( N ` { .0. } ) = { .0. } )
14 9 13 sylan9eqr 
 |-  ( ( ph /\ X = .0. ) -> ( N ` { X } ) = { .0. } )
15 14 ineq1d 
 |-  ( ( ph /\ X = .0. ) -> ( ( N ` { X } ) i^i ( N ` { Y } ) ) = ( { .0. } i^i ( N ` { Y } ) ) )
16 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
17 1 16 3 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
18 11 6 17 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
19 2 16 lss0ss 
 |-  ( ( W e. LMod /\ ( N ` { Y } ) e. ( LSubSp ` W ) ) -> { .0. } C_ ( N ` { Y } ) )
20 11 18 19 syl2anc 
 |-  ( ph -> { .0. } C_ ( N ` { Y } ) )
21 dfss2 
 |-  ( { .0. } C_ ( N ` { Y } ) <-> ( { .0. } i^i ( N ` { Y } ) ) = { .0. } )
22 20 21 sylib 
 |-  ( ph -> ( { .0. } i^i ( N ` { Y } ) ) = { .0. } )
23 22 adantr 
 |-  ( ( ph /\ X = .0. ) -> ( { .0. } i^i ( N ` { Y } ) ) = { .0. } )
24 15 23 eqtrd 
 |-  ( ( ph /\ X = .0. ) -> ( ( N ` { X } ) i^i ( N ` { Y } ) ) = { .0. } )
25 4 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> W e. LVec )
26 18 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
27 5 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> X e. V )
28 7 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
29 25 adantr 
 |-  ( ( ( ph /\ X =/= .0. ) /\ X e. ( N ` { Y } ) ) -> W e. LVec )
30 6 adantr 
 |-  ( ( ph /\ X =/= .0. ) -> Y e. V )
31 30 adantr 
 |-  ( ( ( ph /\ X =/= .0. ) /\ X e. ( N ` { Y } ) ) -> Y e. V )
32 simpr 
 |-  ( ( ( ph /\ X =/= .0. ) /\ X e. ( N ` { Y } ) ) -> X e. ( N ` { Y } ) )
33 simplr 
 |-  ( ( ( ph /\ X =/= .0. ) /\ X e. ( N ` { Y } ) ) -> X =/= .0. )
34 1 2 3 29 31 32 33 lspsneleq 
 |-  ( ( ( ph /\ X =/= .0. ) /\ X e. ( N ` { Y } ) ) -> ( N ` { X } ) = ( N ` { Y } ) )
35 34 ex 
 |-  ( ( ph /\ X =/= .0. ) -> ( X e. ( N ` { Y } ) -> ( N ` { X } ) = ( N ` { Y } ) ) )
36 35 necon3ad 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( N ` { X } ) =/= ( N ` { Y } ) -> -. X e. ( N ` { Y } ) ) )
37 28 36 mpd 
 |-  ( ( ph /\ X =/= .0. ) -> -. X e. ( N ` { Y } ) )
38 1 2 3 16 25 26 27 37 lspdisj 
 |-  ( ( ph /\ X =/= .0. ) -> ( ( N ` { X } ) i^i ( N ` { Y } ) ) = { .0. } )
39 24 38 pm2.61dane 
 |-  ( ph -> ( ( N ` { X } ) i^i ( N ` { Y } ) ) = { .0. } )