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