# 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. } ) )`
` |-  ( 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. } ) )`
` |-  ( ( 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. } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { ( Y .+ Z ) } ) = ( N ` { .0. } ) )`
30 26 29 neeqtrrd
` |-  ( ( ph /\ ( Y .+ Z ) = .0. ) -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X } ) =/= ( N ` { Y } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> W e. LVec )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> X e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> Y e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> Z e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> w e. ( V \ { .0. } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { Y } ) = ( N ` { Z } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> -. w e. ( N ` { X , Y } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( Y .+ Z ) =/= .0. )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) )`
` |-  ( ( ph /\ ( Y .+ Z ) =/= .0. ) -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )`
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )`