Metamath Proof Explorer

Theorem lshpkrlem5

Description: Lemma for lshpkrex . Part of showing linearity of G . (Contributed by NM, 16-Jul-2014)

Ref Expression
Hypotheses lshpkrlem.v 
|- V = ( Base ` W )
lshpkrlem.a 
|- .+ = ( +g ` W )
lshpkrlem.n 
|- N = ( LSpan ` W )
lshpkrlem.p 
|- .(+) = ( LSSum ` W )
lshpkrlem.h 
|- H = ( LSHyp ` W )
lshpkrlem.w 
|- ( ph -> W e. LVec )
lshpkrlem.u 
|- ( ph -> U e. H )
lshpkrlem.z 
|- ( ph -> Z e. V )
lshpkrlem.x 
|- ( ph -> X e. V )
lshpkrlem.e 
|- ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
lshpkrlem.d 
|- D = ( Scalar ` W )
lshpkrlem.k 
|- K = ( Base ` D )
lshpkrlem.t 
|- .x. = ( .s ` W )
lshpkrlem.o 
|- .0. = ( 0g ` D )
lshpkrlem.g 
|- G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
Assertion lshpkrlem5 
|- ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )

Proof

Step Hyp Ref Expression
1 lshpkrlem.v 
 |-  V = ( Base ` W )
2 lshpkrlem.a 
 |-  .+ = ( +g ` W )
3 lshpkrlem.n 
 |-  N = ( LSpan ` W )
4 lshpkrlem.p 
 |-  .(+) = ( LSSum ` W )
5 lshpkrlem.h 
 |-  H = ( LSHyp ` W )
6 lshpkrlem.w 
 |-  ( ph -> W e. LVec )
7 lshpkrlem.u 
 |-  ( ph -> U e. H )
8 lshpkrlem.z 
 |-  ( ph -> Z e. V )
9 lshpkrlem.x 
 |-  ( ph -> X e. V )
10 lshpkrlem.e 
 |-  ( ph -> ( U .(+) ( N ` { Z } ) ) = V )
11 lshpkrlem.d 
 |-  D = ( Scalar ` W )
12 lshpkrlem.k 
 |-  K = ( Base ` D )
13 lshpkrlem.t 
 |-  .x. = ( .s ` W )
14 lshpkrlem.o 
 |-  .0. = ( 0g ` D )
15 lshpkrlem.g 
 |-  G = ( x e. V |-> ( iota_ k e. K E. y e. U x = ( y .+ ( k .x. Z ) ) ) )
16 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
17 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
18 simp11 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ph )
19 18 6 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> W e. LVec )
20 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
21 19 20 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> W e. LMod )
22 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
23 22 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
24 21 23 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
25 6 20 syl 
 |-  ( ph -> W e. LMod )
26 22 5 25 7 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
27 18 26 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> U e. ( LSubSp ` W ) )
28 24 27 sseldd 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> U e. ( SubGrp ` W ) )
29 18 8 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> Z e. V )
30 1 22 3 lspsncl 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
31 21 29 30 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
32 24 31 sseldd 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( N ` { Z } ) e. ( SubGrp ` W ) )
33 1 16 3 4 5 6 7 8 10 lshpdisj 
 |-  ( ph -> ( U i^i ( N ` { Z } ) ) = { ( 0g ` W ) } )
34 18 33 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( U i^i ( N ` { Z } ) ) = { ( 0g ` W ) } )
35 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
36 21 35 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> W e. Abel )
37 17 36 28 32 ablcntzd 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> U C_ ( ( Cntz ` W ) ` ( N ` { Z } ) ) )
38 simp23r 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> z e. U )
39 simp12 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> l e. K )
40 simp22 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> r e. U )
41 11 13 12 22 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. ( LSubSp ` W ) ) /\ ( l e. K /\ r e. U ) ) -> ( l .x. r ) e. U )
42 21 27 39 40 41 syl22anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( l .x. r ) e. U )
43 simp23l 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> s e. U )
44 2 22 lssvacl 
 |-  ( ( ( W e. LMod /\ U e. ( LSubSp ` W ) ) /\ ( ( l .x. r ) e. U /\ s e. U ) ) -> ( ( l .x. r ) .+ s ) e. U )
45 21 27 42 43 44 syl22anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( l .x. r ) .+ s ) e. U )
46 simp13 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> u e. V )
47 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ l e. K /\ u e. V ) -> ( l .x. u ) e. V )
48 21 39 46 47 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( l .x. u ) e. V )
49 simp21 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> v e. V )
50 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ ( l .x. u ) e. V /\ v e. V ) -> ( ( l .x. u ) .+ v ) e. V )
51 21 48 49 50 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) e. V )
52 6 adantr 
 |-  ( ( ph /\ ( ( l .x. u ) .+ v ) e. V ) -> W e. LVec )
53 7 adantr 
 |-  ( ( ph /\ ( ( l .x. u ) .+ v ) e. V ) -> U e. H )
54 8 adantr 
 |-  ( ( ph /\ ( ( l .x. u ) .+ v ) e. V ) -> Z e. V )
55 simpr 
 |-  ( ( ph /\ ( ( l .x. u ) .+ v ) e. V ) -> ( ( l .x. u ) .+ v ) e. V )
56 10 adantr 
 |-  ( ( ph /\ ( ( l .x. u ) .+ v ) e. V ) -> ( U .(+) ( N ` { Z } ) ) = V )
57 1 2 3 4 5 52 53 54 55 56 11 12 13 14 15 lshpkrlem2 
 |-  ( ( ph /\ ( ( l .x. u ) .+ v ) e. V ) -> ( G ` ( ( l .x. u ) .+ v ) ) e. K )
58 18 51 57 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) e. K )
59 1 13 11 12 3 21 58 29 lspsneli 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) e. ( N ` { Z } ) )
60 6 adantr 
 |-  ( ( ph /\ u e. V ) -> W e. LVec )
61 7 adantr 
 |-  ( ( ph /\ u e. V ) -> U e. H )
62 8 adantr 
 |-  ( ( ph /\ u e. V ) -> Z e. V )
63 simpr 
 |-  ( ( ph /\ u e. V ) -> u e. V )
64 10 adantr 
 |-  ( ( ph /\ u e. V ) -> ( U .(+) ( N ` { Z } ) ) = V )
65 1 2 3 4 5 60 61 62 63 64 11 12 13 14 15 lshpkrlem2 
 |-  ( ( ph /\ u e. V ) -> ( G ` u ) e. K )
66 18 46 65 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` u ) e. K )
67 eqid 
 |-  ( .r ` D ) = ( .r ` D )
68 11 12 67 lmodmcl 
 |-  ( ( W e. LMod /\ l e. K /\ ( G ` u ) e. K ) -> ( l ( .r ` D ) ( G ` u ) ) e. K )
69 21 39 66 68 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( l ( .r ` D ) ( G ` u ) ) e. K )
70 6 adantr 
 |-  ( ( ph /\ v e. V ) -> W e. LVec )
71 7 adantr 
 |-  ( ( ph /\ v e. V ) -> U e. H )
72 8 adantr 
 |-  ( ( ph /\ v e. V ) -> Z e. V )
73 simpr 
 |-  ( ( ph /\ v e. V ) -> v e. V )
74 10 adantr 
 |-  ( ( ph /\ v e. V ) -> ( U .(+) ( N ` { Z } ) ) = V )
75 1 2 3 4 5 70 71 72 73 74 11 12 13 14 15 lshpkrlem2 
 |-  ( ( ph /\ v e. V ) -> ( G ` v ) e. K )
76 18 49 75 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` v ) e. K )
77 eqid 
 |-  ( +g ` D ) = ( +g ` D )
78 11 12 77 lmodacl 
 |-  ( ( W e. LMod /\ ( l ( .r ` D ) ( G ` u ) ) e. K /\ ( G ` v ) e. K ) -> ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) e. K )
79 21 69 76 78 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) e. K )
80 1 13 11 12 3 21 79 29 lspsneli 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) e. ( N ` { Z } ) )
81 simp33 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) )
82 simp1 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ph /\ l e. K /\ u e. V ) )
83 1 22 lssel 
 |-  ( ( U e. ( LSubSp ` W ) /\ r e. U ) -> r e. V )
84 27 40 83 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> r e. V )
85 1 22 lssel 
 |-  ( ( U e. ( LSubSp ` W ) /\ s e. U ) -> s e. V )
86 27 43 85 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> s e. V )
87 simp31 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> u = ( r .+ ( ( G ` u ) .x. Z ) ) )
88 simp32 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> v = ( s .+ ( ( G ` v ) .x. Z ) ) )
89 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lshpkrlem4 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
90 82 49 84 86 87 88 89 syl132anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( l .x. u ) .+ v ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
91 81 90 eqtr3d 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
92 2 16 17 28 32 34 37 38 45 59 80 91 subgdisj2 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) = ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) )
93 1 3 4 5 16 25 7 8 10 lshpne0 
 |-  ( ph -> Z =/= ( 0g ` W ) )
94 18 93 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> Z =/= ( 0g ` W ) )
95 1 13 11 12 16 19 58 79 29 94 lvecvscan2 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) = ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) <-> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) ) )
96 92 95 mpbid 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. U /\ ( s e. U /\ z e. U ) ) /\ ( u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )