Metamath Proof Explorer

Theorem mapdindp1

Description: Vector independence lemma. (Contributed by NM, 1-May-2015)

Ref Expression
Hypotheses mapdindp1.v 
|- V = ( Base ` W )
mapdindp1.p 
|- .+ = ( +g ` W )
mapdindp1.o 
|- .0. = ( 0g ` W )
mapdindp1.n 
|- N = ( LSpan ` W )
mapdindp1.w 
|- ( ph -> W e. LVec )
mapdindp1.x 
|- ( ph -> X e. ( V \ { .0. } ) )
mapdindp1.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
mapdindp1.z 
|- ( ph -> Z e. ( V \ { .0. } ) )
mapdindp1.W 
|- ( ph -> w e. ( V \ { .0. } ) )
mapdindp1.e 
|- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )
mapdindp1.ne 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
mapdindp1.f 
|- ( ph -> -. w e. ( N ` { X , Y } ) )
Assertion mapdindp1 
|- ( ph -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )

Proof

Step Hyp Ref Expression
1 mapdindp1.v 
 |-  V = ( Base ` W )
2 mapdindp1.p 
 |-  .+ = ( +g ` W )
3 mapdindp1.o 
 |-  .0. = ( 0g ` W )
4 mapdindp1.n 
 |-  N = ( LSpan ` W )
5 mapdindp1.w 
 |-  ( ph -> W e. LVec )
6 mapdindp1.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
7 mapdindp1.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
8 mapdindp1.z 
 |-  ( ph -> Z e. ( V \ { .0. } ) )
9 mapdindp1.W 
 |-  ( ph -> w e. ( V \ { .0. } ) )
10 mapdindp1.e 
 |-  ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )
11 mapdindp1.ne 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
12 mapdindp1.f 
 |-  ( ph -> -. w e. ( N ` { X , Y } ) )
13 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
14 6 13 syl 
 |-  ( ph -> X =/= .0. )
15 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
16 5 15 syl 
 |-  ( ph -> W e. LMod )
17 3 4 lspsn0 
 |-  ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
18 16 17 syl 
 |-  ( ph -> ( N ` { .0. } ) = { .0. } )
19 18 eqeq2d 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { .0. } ) <-> ( N ` { X } ) = { .0. } ) )
20 6 eldifad 
 |-  ( ph -> X e. V )
21 1 3 4 lspsneq0 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
22 16 20 21 syl2anc 
 |-  ( ph -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
23 19 22 bitrd 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { .0. } ) <-> X = .0. ) )
24 23 necon3bid 
 |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { .0. } ) <-> X =/= .0. ) )
25 14 24 mpbird 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { .0. } ) )
26 25 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { X } ) =/= ( N ` { .0. } ) )
27 sneq 
 |-  ( ( Y .+ Z ) = .0. -> { ( Y .+ Z ) } = { .0. } )
28 27 fveq2d 
 |-  ( ( Y .+ Z ) = .0. -> ( N ` { ( Y .+ Z ) } ) = ( N ` { .0. } ) )
29 28 adantl 
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { ( Y .+ Z ) } ) = ( N ` { .0. } ) )
30 26 29 neeqtrrd 
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )
31 11 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
32 5 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> W e. LVec )
33 6 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> X e. ( V \ { .0. } ) )
34 7 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> Y e. ( V \ { .0. } ) )
35 8 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> Z e. ( V \ { .0. } ) )
36 9 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> w e. ( V \ { .0. } ) )
37 10 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { Y } ) = ( N ` { Z } ) )
38 12 adantr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> -. w e. ( N ` { X , Y } ) )
39 simpr 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( Y .+ Z ) =/= .0. )
40 1 2 3 4 32 33 34 35 36 37 31 38 39 mapdindp0 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) )
41 31 40 neeqtrrd 
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )
42 30 41 pm2.61dane 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )