Metamath Proof Explorer

Theorem lshpkrlem6

Description: Lemma for lshpkrex . Show linearlity of G . (Contributed by NM, 17-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 lshpkrlem6 
|- ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( 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 6 adantr 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> W e. LVec )
17 7 adantr 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> U e. H )
18 8 adantr 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> Z e. V )
19 simpr2 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> u e. V )
20 10 adantr 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( U .(+) ( N ` { Z } ) ) = V )
21 1 2 3 4 5 16 17 18 19 20 11 12 13 14 15 lshpkrlem3 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> E. r e. U u = ( r .+ ( ( G ` u ) .x. Z ) ) )
22 simpr3 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> v e. V )
23 1 2 3 4 5 16 17 18 22 20 11 12 13 14 15 lshpkrlem3 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> E. s e. U v = ( s .+ ( ( G ` v ) .x. Z ) ) )
24 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
25 16 24 syl 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> W e. LMod )
26 simpr1 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> l e. K )
27 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ l e. K /\ u e. V ) -> ( l .x. u ) e. V )
28 25 26 19 27 syl3anc 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( l .x. u ) e. V )
29 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ ( l .x. u ) e. V /\ v e. V ) -> ( ( l .x. u ) .+ v ) e. V )
30 25 28 22 29 syl3anc 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( ( l .x. u ) .+ v ) e. V )
31 1 2 3 4 5 16 17 18 30 20 11 12 13 14 15 lshpkrlem3 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> E. z e. U ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) )
32 3reeanv 
 |-  ( E. r e. U E. s e. U E. 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 ) ) ) <-> ( E. r e. U u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ E. s e. U v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ E. z e. U ( ( l .x. u ) .+ v ) = ( z .+ ( ( G ` ( ( l .x. u ) .+ v ) ) .x. Z ) ) ) )
33 simp1l 
 |-  ( ( ( 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 )
34 simp1r1 
 |-  ( ( ( 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 )
35 simp1r2 
 |-  ( ( ( 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 )
36 simp1r3 
 |-  ( ( ( 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 )
37 simp2ll 
 |-  ( ( ( 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 )
38 simp2lr 
 |-  ( ( ( 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 )
39 simp2r 
 |-  ( ( ( 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 )
40 38 39 jca 
 |-  ( ( ( 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 /\ z e. U ) )
41 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 ) ) )
42 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 ) ) )
43 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 ) ) )
44 1 2 3 4 5 6 7 8 8 10 11 12 13 14 15 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 ) ) )
45 33 34 35 36 37 40 41 42 43 44 syl333anc 
 |-  ( ( ( 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 ) ) )
46 45 3exp 
 |-  ( ( 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 ) ) ) ) )
47 46 expdimp 
 |-  ( ( ( 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 ) ) ) ) )
48 47 rexlimdv 
 |-  ( ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) /\ ( r e. U /\ s e. U ) ) -> ( E. 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 ) ) ) )
49 48 rexlimdvva 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( E. r e. U E. s e. U E. 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 ) ) ) )
50 32 49 biimtrrid 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( ( E. r e. U u = ( r .+ ( ( G ` u ) .x. Z ) ) /\ E. s e. U v = ( s .+ ( ( G ` v ) .x. Z ) ) /\ E. z e. U ( ( 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 ) ) ) )
51 21 23 31 50 mp3and 
 |-  ( ( ph /\ ( l e. K /\ u e. V /\ v e. V ) ) -> ( G ` ( ( l .x. u ) .+ v ) ) = ( ( l ( .r ` D ) ( G ` u ) ) ( +g ` D ) ( G ` v ) ) )