Metamath Proof Explorer

Theorem mapdindp3

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 mapdindp3 
|- ( ph -> ( N ` { X } ) =/= ( N ` { ( 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 4 lspvadd 
 |-  ( ( W e. LMod /\ w e. V /\ Y e. V ) -> ( N ` { ( w .+ Y ) } ) C_ ( N ` { w , Y } ) )
18 14 15 16 17 syl3anc 
 |-  ( ph -> ( N ` { ( w .+ Y ) } ) C_ ( N ` { w , Y } ) )
19 1 3 4 5 6 16 15 11 12 lspindp1 
 |-  ( ph -> ( ( N ` { w } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { w , Y } ) ) )
20 19 simprd 
 |-  ( ph -> -. X e. ( N ` { w , Y } ) )
21 18 20 ssneldd 
 |-  ( ph -> -. X e. ( N ` { ( w .+ Y ) } ) )
22 6 eldifad 
 |-  ( ph -> X e. V )
23 1 4 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
24 14 22 23 syl2anc 
 |-  ( ph -> X e. ( N ` { X } ) )
25 eleq2 
 |-  ( ( N ` { X } ) = ( N ` { ( w .+ Y ) } ) -> ( X e. ( N ` { X } ) <-> X e. ( N ` { ( w .+ Y ) } ) ) )
26 24 25 syl5ibcom 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { ( w .+ Y ) } ) -> X e. ( N ` { ( w .+ Y ) } ) ) )
27 26 necon3bd 
 |-  ( ph -> ( -. X e. ( N ` { ( w .+ Y ) } ) -> ( N ` { X } ) =/= ( N ` { ( w .+ Y ) } ) ) )
28 21 27 mpd 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { ( w .+ Y ) } ) )