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