# Metamath Proof Explorer

## Theorem mapdindp4

Description: Vector independence lemma. (Contributed by NM, 29-Apr-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 mapdindp4
`|- ( ph -> -. Z e. ( N ` { X , ( w .+ Y ) } ) )`

### 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 lveclmod
` |-  ( W e. LVec -> W e. LMod )`
14 5 13 syl
` |-  ( ph -> W e. LMod )`
` |-  ( ph -> w e. V )`
` |-  ( ph -> Y e. V )`
17 1 2 lmodvacl
` |-  ( ( W e. LMod /\ w e. V /\ Y e. V ) -> ( w .+ Y ) e. V )`
18 14 15 16 17 syl3anc
` |-  ( ph -> ( w .+ Y ) e. V )`
` |-  ( ph -> X e. V )`
20 1 4 5 15 19 16 12 lspindpi
` |-  ( ph -> ( ( N ` { w } ) =/= ( N ` { X } ) /\ ( N ` { w } ) =/= ( N ` { Y } ) ) )`
21 20 simprd
` |-  ( ph -> ( N ` { w } ) =/= ( N ` { Y } ) )`
22 21 necomd
` |-  ( ph -> ( N ` { Y } ) =/= ( N ` { w } ) )`
23 1 2 3 4 5 16 9 22 lspindp3
` |-  ( ph -> ( N ` { Y } ) =/= ( N ` { ( Y .+ w ) } ) )`
24 1 2 lmodcom
` |-  ( ( W e. LMod /\ w e. V /\ Y e. V ) -> ( w .+ Y ) = ( Y .+ w ) )`
25 14 15 16 24 syl3anc
` |-  ( ph -> ( w .+ Y ) = ( Y .+ w ) )`
26 25 sneqd
` |-  ( ph -> { ( w .+ Y ) } = { ( Y .+ w ) } )`
27 26 fveq2d
` |-  ( ph -> ( N ` { ( w .+ Y ) } ) = ( N ` { ( Y .+ w ) } ) )`
28 23 27 neeqtrrd
` |-  ( ph -> ( N ` { Y } ) =/= ( N ` { ( w .+ Y ) } ) )`
29 10 28 eqnetrrd
` |-  ( ph -> ( N ` { Z } ) =/= ( N ` { ( w .+ Y ) } ) )`
30 1 3 4 5 6 16 15 11 12 lspindp1
` |-  ( ph -> ( ( N ` { w } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { w , Y } ) ) )`
31 30 simprd
` |-  ( ph -> -. X e. ( N ` { w , Y } ) )`
32 eqid
` |-  ( LSSum ` W ) = ( LSSum ` W )`
` |-  ( ph -> Z e. V )`
34 1 4 32 14 33 18 lsmpr
` |-  ( ph -> ( N ` { Z , ( w .+ Y ) } ) = ( ( N ` { Z } ) ( LSSum ` W ) ( N ` { ( w .+ Y ) } ) ) )`
35 1 2 lmodcom
` |-  ( ( W e. LMod /\ Y e. V /\ w e. V ) -> ( Y .+ w ) = ( w .+ Y ) )`
36 14 16 15 35 syl3anc
` |-  ( ph -> ( Y .+ w ) = ( w .+ Y ) )`
37 36 preq2d
` |-  ( ph -> { Y , ( Y .+ w ) } = { Y , ( w .+ Y ) } )`
38 37 fveq2d
` |-  ( ph -> ( N ` { Y , ( Y .+ w ) } ) = ( N ` { Y , ( w .+ Y ) } ) )`
39 1 2 4 14 16 15 lspprabs
` |-  ( ph -> ( N ` { Y , ( Y .+ w ) } ) = ( N ` { Y , w } ) )`
40 1 4 32 14 16 18 lsmpr
` |-  ( ph -> ( N ` { Y , ( w .+ Y ) } ) = ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { ( w .+ Y ) } ) ) )`
41 38 39 40 3eqtr3rd
` |-  ( ph -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { ( w .+ Y ) } ) ) = ( N ` { Y , w } ) )`
42 10 oveq1d
` |-  ( ph -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { ( w .+ Y ) } ) ) = ( ( N ` { Z } ) ( LSSum ` W ) ( N ` { ( w .+ Y ) } ) ) )`
43 prcom
` |-  { Y , w } = { w , Y }`
44 43 fveq2i
` |-  ( N ` { Y , w } ) = ( N ` { w , Y } )`
45 44 a1i
` |-  ( ph -> ( N ` { Y , w } ) = ( N ` { w , Y } ) )`
46 41 42 45 3eqtr3d
` |-  ( ph -> ( ( N ` { Z } ) ( LSSum ` W ) ( N ` { ( w .+ Y ) } ) ) = ( N ` { w , Y } ) )`
47 34 46 eqtrd
` |-  ( ph -> ( N ` { Z , ( w .+ Y ) } ) = ( N ` { w , Y } ) )`
48 31 47 neleqtrrd
` |-  ( ph -> -. X e. ( N ` { Z , ( w .+ Y ) } ) )`
49 1 3 4 5 8 18 19 29 48 lspindp1
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { ( w .+ Y ) } ) /\ -. Z e. ( N ` { X , ( w .+ Y ) } ) ) )`
50 49 simprd
` |-  ( ph -> -. Z e. ( N ` { X , ( w .+ Y ) } ) )`