Metamath Proof Explorer

Theorem lshpkrlem4

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 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 ) ) )

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 simp3l 
 |-  ( ( ( 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 ) ) ) ) -> u = ( r .+ ( ( G ` u ) .x. Z ) ) )
17 16 oveq2d 
 |-  ( ( ( 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 ) = ( l .x. ( r .+ ( ( G ` u ) .x. Z ) ) ) )
18 simp3r 
 |-  ( ( ( 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 ) ) ) ) -> v = ( s .+ ( ( G ` v ) .x. Z ) ) )
19 17 18 oveq12d 
 |-  ( ( ( 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 .+ ( ( G ` u ) .x. Z ) ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) )
20 simpl1 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ph )
21 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
22 20 6 21 3syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> W e. LMod )
23 simpl2 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> l e. K )
24 simpr2 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> r e. V )
25 simpl3 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> u e. V )
26 6 adantr 
 |-  ( ( ph /\ u e. V ) -> W e. LVec )
27 7 adantr 
 |-  ( ( ph /\ u e. V ) -> U e. H )
28 8 adantr 
 |-  ( ( ph /\ u e. V ) -> Z e. V )
29 simpr 
 |-  ( ( ph /\ u e. V ) -> u e. V )
30 10 adantr 
 |-  ( ( ph /\ u e. V ) -> ( U .(+) ( N ` { Z } ) ) = V )
31 1 2 3 4 5 26 27 28 29 30 11 12 13 14 15 lshpkrlem2 
 |-  ( ( ph /\ u e. V ) -> ( G ` u ) e. K )
32 20 25 31 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( G ` u ) e. K )
33 20 8 syl 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> Z e. V )
34 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ ( G ` u ) e. K /\ Z e. V ) -> ( ( G ` u ) .x. Z ) e. V )
35 22 32 33 34 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( G ` u ) .x. Z ) e. V )
36 1 2 11 13 12 lmodvsdi 
 |-  ( ( W e. LMod /\ ( l e. K /\ r e. V /\ ( ( G ` u ) .x. Z ) e. V ) ) -> ( l .x. ( r .+ ( ( G ` u ) .x. Z ) ) ) = ( ( l .x. r ) .+ ( l .x. ( ( G ` u ) .x. Z ) ) ) )
37 22 23 24 35 36 syl13anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( l .x. ( r .+ ( ( G ` u ) .x. Z ) ) ) = ( ( l .x. r ) .+ ( l .x. ( ( G ` u ) .x. Z ) ) ) )
38 eqid 
 |-  ( .r ` D ) = ( .r ` D )
39 1 11 13 12 38 lmodvsass 
 |-  ( ( W e. LMod /\ ( l e. K /\ ( G ` u ) e. K /\ Z e. V ) ) -> ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) = ( l .x. ( ( G ` u ) .x. Z ) ) )
40 22 23 32 33 39 syl13anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) = ( l .x. ( ( G ` u ) .x. Z ) ) )
41 40 oveq2d 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( l .x. r ) .+ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) ) = ( ( l .x. r ) .+ ( l .x. ( ( G ` u ) .x. Z ) ) ) )
42 37 41 eqtr4d 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( l .x. ( r .+ ( ( G ` u ) .x. Z ) ) ) = ( ( l .x. r ) .+ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) ) )
43 42 oveq1d 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( l .x. ( r .+ ( ( G ` u ) .x. Z ) ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) = ( ( ( l .x. r ) .+ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) )
44 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ l e. K /\ r e. V ) -> ( l .x. r ) e. V )
45 22 23 24 44 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( l .x. r ) e. V )
46 11 12 38 lmodmcl 
 |-  ( ( W e. LMod /\ l e. K /\ ( G ` u ) e. K ) -> ( l ( .r ` D ) ( G ` u ) ) e. K )
47 22 23 32 46 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( l ( .r ` D ) ( G ` u ) ) e. K )
48 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ ( l ( .r ` D ) ( G ` u ) ) e. K /\ Z e. V ) -> ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) e. V )
49 22 47 33 48 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) e. V )
50 simpr3 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> s e. V )
51 simpr1 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> v e. V )
52 6 adantr 
 |-  ( ( ph /\ v e. V ) -> W e. LVec )
53 7 adantr 
 |-  ( ( ph /\ v e. V ) -> U e. H )
54 8 adantr 
 |-  ( ( ph /\ v e. V ) -> Z e. V )
55 simpr 
 |-  ( ( ph /\ v e. V ) -> v e. V )
56 10 adantr 
 |-  ( ( ph /\ 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 /\ v e. V ) -> ( G ` v ) e. K )
58 20 51 57 syl2anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( G ` v ) e. K )
59 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ ( G ` v ) e. K /\ Z e. V ) -> ( ( G ` v ) .x. Z ) e. V )
60 22 58 33 59 syl3anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( G ` v ) .x. Z ) e. V )
61 1 2 lmod4 
 |-  ( ( W e. LMod /\ ( ( l .x. r ) e. V /\ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) e. V ) /\ ( s e. V /\ ( ( G ` v ) .x. Z ) e. V ) ) -> ( ( ( l .x. r ) .+ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) .+ ( ( G ` v ) .x. Z ) ) ) )
62 22 45 49 50 60 61 syl122anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( ( l .x. r ) .+ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) .+ ( ( G ` v ) .x. Z ) ) ) )
63 eqid 
 |-  ( +g ` D ) = ( +g ` D )
64 1 2 11 13 12 63 lmodvsdir 
 |-  ( ( W e. LMod /\ ( ( l ( .r ` D ) ( G ` u ) ) e. K /\ ( G ` v ) e. K /\ Z e. V ) ) -> ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) = ( ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) .+ ( ( G ` v ) .x. Z ) ) )
65 22 47 58 33 64 syl13anc 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) = ( ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) .+ ( ( G ` v ) .x. Z ) ) )
66 65 oveq2d 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) .+ ( ( G ` v ) .x. Z ) ) ) )
67 62 66 eqtr4d 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( ( l .x. r ) .+ ( ( l ( .r ` D ) ( G ` u ) ) .x. Z ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
68 43 67 eqtrd 
 |-  ( ( ( ph /\ l e. K /\ u e. V ) /\ ( v e. V /\ r e. V /\ s e. V ) ) -> ( ( l .x. ( r .+ ( ( G ` u ) .x. Z ) ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
69 68 3adant3 
 |-  ( ( ( 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. ( r .+ ( ( G ` u ) .x. Z ) ) ) .+ ( s .+ ( ( G ` v ) .x. Z ) ) ) = ( ( ( l .x. r ) .+ s ) .+ ( ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) .x. Z ) ) )
70 19 69 eqtrd 
 |-  ( ( ( 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 ) ) )