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 )
15 9 eldifad
 |-  ( ph -> w e. V )
16 7 eldifad
 |-  ( 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 )
19 6 eldifad
 |-  ( 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 )
33 8 eldifad
 |-  ( 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 ) } ) )