Metamath Proof Explorer

Theorem mapdindp0

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 } ) )
mapdindp1.yz 
|- ( ph -> ( Y .+ Z ) =/= .0. )
Assertion mapdindp0 
|- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( N ` { 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 mapdindp1.yz 
 |-  ( ph -> ( Y .+ Z ) =/= .0. )
14 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
15 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
16 5 15 syl 
 |-  ( ph -> W e. LMod )
17 7 eldifad 
 |-  ( ph -> Y e. V )
18 1 14 4 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
19 16 17 18 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
20 10 19 eqeltrrd 
 |-  ( ph -> ( N ` { Z } ) e. ( LSubSp ` W ) )
21 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
22 14 21 lsmcl 
 |-  ( ( W e. LMod /\ ( N ` { Y } ) e. ( LSubSp ` W ) /\ ( N ` { Z } ) e. ( LSubSp ` W ) ) -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) e. ( LSubSp ` W ) )
23 16 19 20 22 syl3anc 
 |-  ( ph -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) e. ( LSubSp ` W ) )
24 14 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
25 16 24 syl 
 |-  ( ph -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
26 25 19 sseldd 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
27 10 26 eqeltrrd 
 |-  ( ph -> ( N ` { Z } ) e. ( SubGrp ` W ) )
28 1 4 lspsnid 
 |-  ( ( W e. LMod /\ Y e. V ) -> Y e. ( N ` { Y } ) )
29 16 17 28 syl2anc 
 |-  ( ph -> Y e. ( N ` { Y } ) )
30 8 eldifad 
 |-  ( ph -> Z e. V )
31 1 4 lspsnid 
 |-  ( ( W e. LMod /\ Z e. V ) -> Z e. ( N ` { Z } ) )
32 16 30 31 syl2anc 
 |-  ( ph -> Z e. ( N ` { Z } ) )
33 2 21 lsmelvali 
 |-  ( ( ( ( N ` { Y } ) e. ( SubGrp ` W ) /\ ( N ` { Z } ) e. ( SubGrp ` W ) ) /\ ( Y e. ( N ` { Y } ) /\ Z e. ( N ` { Z } ) ) ) -> ( Y .+ Z ) e. ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
34 26 27 29 32 33 syl22anc 
 |-  ( ph -> ( Y .+ Z ) e. ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
35 14 4 16 23 34 ellspsn5 
 |-  ( ph -> ( N ` { ( Y .+ Z ) } ) C_ ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
36 10 oveq2d 
 |-  ( ph -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Y } ) ) = ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
37 21 lsmidm 
 |-  ( ( N ` { Y } ) e. ( SubGrp ` W ) -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Y } ) ) = ( N ` { Y } ) )
38 26 37 syl 
 |-  ( ph -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Y } ) ) = ( N ` { Y } ) )
39 36 38 eqtr3d 
 |-  ( ph -> ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) = ( N ` { Y } ) )
40 35 39 sseqtrd 
 |-  ( ph -> ( N ` { ( Y .+ Z ) } ) C_ ( N ` { Y } ) )
41 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
42 16 17 30 41 syl3anc 
 |-  ( ph -> ( Y .+ Z ) e. V )
43 eldifsn 
 |-  ( ( Y .+ Z ) e. ( V \ { .0. } ) <-> ( ( Y .+ Z ) e. V /\ ( Y .+ Z ) =/= .0. ) )
44 42 13 43 sylanbrc 
 |-  ( ph -> ( Y .+ Z ) e. ( V \ { .0. } ) )
45 1 3 4 5 44 17 lspsncmp 
 |-  ( ph -> ( ( N ` { ( Y .+ Z ) } ) C_ ( N ` { Y } ) <-> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) ) )
46 40 45 mpbid 
 |-  ( ph -> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) )