Metamath Proof Explorer


Theorem mapdindp2

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 mapdindp2
|- ( ph -> -. w e. ( N ` { X , ( 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 preq2
 |-  ( ( Y .+ Z ) = .0. -> { X , ( Y .+ Z ) } = { X , .0. } )
14 13 fveq2d
 |-  ( ( Y .+ Z ) = .0. -> ( N ` { X , ( Y .+ Z ) } ) = ( N ` { X , .0. } ) )
15 lveclmod
 |-  ( W e. LVec -> W e. LMod )
16 5 15 syl
 |-  ( ph -> W e. LMod )
17 6 eldifad
 |-  ( ph -> X e. V )
18 1 3 4 16 17 lsppr0
 |-  ( ph -> ( N ` { X , .0. } ) = ( N ` { X } ) )
19 14 18 sylan9eqr
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { X , ( Y .+ Z ) } ) = ( N ` { X } ) )
20 7 eldifad
 |-  ( ph -> Y e. V )
21 prssi
 |-  ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
22 17 20 21 syl2anc
 |-  ( ph -> { X , Y } C_ V )
23 snsspr1
 |-  { X } C_ { X , Y }
24 23 a1i
 |-  ( ph -> { X } C_ { X , Y } )
25 1 4 lspss
 |-  ( ( W e. LMod /\ { X , Y } C_ V /\ { X } C_ { X , Y } ) -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
26 16 22 24 25 syl3anc
 |-  ( ph -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
27 26 adantr
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
28 19 27 eqsstrd
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { X , ( Y .+ Z ) } ) C_ ( N ` { X , Y } ) )
29 12 adantr
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> -. w e. ( N ` { X , Y } ) )
30 28 29 ssneldd
 |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> -. w e. ( N ` { X , ( Y .+ Z ) } ) )
31 12 adantr
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> -. w e. ( N ` { X , 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 11 adantr
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
39 simpr
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( Y .+ Z ) =/= .0. )
40 1 2 3 4 32 33 34 35 36 37 38 31 39 mapdindp0
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) )
41 40 oveq2d
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( Y .+ Z ) } ) ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
42 eqid
 |-  ( LSSum ` W ) = ( LSSum ` W )
43 8 eldifad
 |-  ( ph -> Z e. V )
44 1 2 lmodvacl
 |-  ( ( W e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
45 16 20 43 44 syl3anc
 |-  ( ph -> ( Y .+ Z ) e. V )
46 1 4 42 16 17 45 lsmpr
 |-  ( ph -> ( N ` { X , ( Y .+ Z ) } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( Y .+ Z ) } ) ) )
47 46 adantr
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X , ( Y .+ Z ) } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( Y .+ Z ) } ) ) )
48 1 4 42 16 17 20 lsmpr
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
49 48 adantr
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
50 41 47 49 3eqtr4d
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X , ( Y .+ Z ) } ) = ( N ` { X , Y } ) )
51 31 50 neleqtrrd
 |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> -. w e. ( N ` { X , ( Y .+ Z ) } ) )
52 30 51 pm2.61dane
 |-  ( ph -> -. w e. ( N ` { X , ( Y .+ Z ) } ) )