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 df-ss
 |-  ( { .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. } )