Step |
Hyp |
Ref |
Expression |
1 |
|
hdmaprnlem1.h |
|- H = ( LHyp ` K ) |
2 |
|
hdmaprnlem1.u |
|- U = ( ( DVecH ` K ) ` W ) |
3 |
|
hdmaprnlem1.v |
|- V = ( Base ` U ) |
4 |
|
hdmaprnlem1.n |
|- N = ( LSpan ` U ) |
5 |
|
hdmaprnlem1.c |
|- C = ( ( LCDual ` K ) ` W ) |
6 |
|
hdmaprnlem1.l |
|- L = ( LSpan ` C ) |
7 |
|
hdmaprnlem1.m |
|- M = ( ( mapd ` K ) ` W ) |
8 |
|
hdmaprnlem1.s |
|- S = ( ( HDMap ` K ) ` W ) |
9 |
|
hdmaprnlem1.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
10 |
|
hdmaprnlem1.se |
|- ( ph -> s e. ( D \ { Q } ) ) |
11 |
|
hdmaprnlem1.ve |
|- ( ph -> v e. V ) |
12 |
|
hdmaprnlem1.e |
|- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) |
13 |
|
hdmaprnlem1.ue |
|- ( ph -> u e. V ) |
14 |
|
hdmaprnlem1.un |
|- ( ph -> -. u e. ( N ` { v } ) ) |
15 |
|
hdmaprnlem1.d |
|- D = ( Base ` C ) |
16 |
|
hdmaprnlem1.q |
|- Q = ( 0g ` C ) |
17 |
|
hdmaprnlem1.o |
|- .0. = ( 0g ` U ) |
18 |
|
hdmaprnlem1.a |
|- .+b = ( +g ` C ) |
19 |
|
hdmaprnlem3e.p |
|- .+ = ( +g ` U ) |
20 |
|
eqid |
|- ( LSAtoms ` U ) = ( LSAtoms ` U ) |
21 |
1 2 9
|
dvhlvec |
|- ( ph -> U e. LVec ) |
22 |
|
eqid |
|- ( LSAtoms ` C ) = ( LSAtoms ` C ) |
23 |
1 5 9
|
lcdlmod |
|- ( ph -> C e. LMod ) |
24 |
1 2 3 5 15 8 9 13
|
hdmapcl |
|- ( ph -> ( S ` u ) e. D ) |
25 |
10
|
eldifad |
|- ( ph -> s e. D ) |
26 |
15 18
|
lmodvacl |
|- ( ( C e. LMod /\ ( S ` u ) e. D /\ s e. D ) -> ( ( S ` u ) .+b s ) e. D ) |
27 |
23 24 25 26
|
syl3anc |
|- ( ph -> ( ( S ` u ) .+b s ) e. D ) |
28 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14
|
hdmaprnlem1N |
|- ( ph -> ( L ` { ( S ` u ) } ) =/= ( L ` { s } ) ) |
29 |
15 18 16 6 23 24 25 28
|
lmodindp1 |
|- ( ph -> ( ( S ` u ) .+b s ) =/= Q ) |
30 |
|
eldifsn |
|- ( ( ( S ` u ) .+b s ) e. ( D \ { Q } ) <-> ( ( ( S ` u ) .+b s ) e. D /\ ( ( S ` u ) .+b s ) =/= Q ) ) |
31 |
27 29 30
|
sylanbrc |
|- ( ph -> ( ( S ` u ) .+b s ) e. ( D \ { Q } ) ) |
32 |
15 6 16 22 23 31
|
lsatlspsn |
|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSAtoms ` C ) ) |
33 |
1 7 2 20 5 22 9 32
|
mapdcnvatN |
|- ( ph -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) e. ( LSAtoms ` U ) ) |
34 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
|
hdmaprnlem3uN |
|- ( ph -> ( N ` { u } ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) ) |
35 |
34
|
necomd |
|- ( ph -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) =/= ( N ` { u } ) ) |
36 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
|
hdmaprnlem3N |
|- ( ph -> ( N ` { v } ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) ) |
37 |
36
|
necomd |
|- ( ph -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) =/= ( N ` { v } ) ) |
38 |
|
eqid |
|- ( LSubSp ` C ) = ( LSubSp ` C ) |
39 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
40 |
1 2 9
|
dvhlmod |
|- ( ph -> U e. LMod ) |
41 |
3 39 4
|
lspsncl |
|- ( ( U e. LMod /\ u e. V ) -> ( N ` { u } ) e. ( LSubSp ` U ) ) |
42 |
40 13 41
|
syl2anc |
|- ( ph -> ( N ` { u } ) e. ( LSubSp ` U ) ) |
43 |
1 7 2 39 5 38 9 42
|
mapdcl2 |
|- ( ph -> ( M ` ( N ` { u } ) ) e. ( LSubSp ` C ) ) |
44 |
3 39 4
|
lspsncl |
|- ( ( U e. LMod /\ v e. V ) -> ( N ` { v } ) e. ( LSubSp ` U ) ) |
45 |
40 11 44
|
syl2anc |
|- ( ph -> ( N ` { v } ) e. ( LSubSp ` U ) ) |
46 |
1 7 2 39 5 38 9 45
|
mapdcl2 |
|- ( ph -> ( M ` ( N ` { v } ) ) e. ( LSubSp ` C ) ) |
47 |
|
eqid |
|- ( LSSum ` C ) = ( LSSum ` C ) |
48 |
38 47
|
lsmcl |
|- ( ( C e. LMod /\ ( M ` ( N ` { u } ) ) e. ( LSubSp ` C ) /\ ( M ` ( N ` { v } ) ) e. ( LSubSp ` C ) ) -> ( ( M ` ( N ` { u } ) ) ( LSSum ` C ) ( M ` ( N ` { v } ) ) ) e. ( LSubSp ` C ) ) |
49 |
23 43 46 48
|
syl3anc |
|- ( ph -> ( ( M ` ( N ` { u } ) ) ( LSSum ` C ) ( M ` ( N ` { v } ) ) ) e. ( LSubSp ` C ) ) |
50 |
38
|
lsssssubg |
|- ( C e. LMod -> ( LSubSp ` C ) C_ ( SubGrp ` C ) ) |
51 |
23 50
|
syl |
|- ( ph -> ( LSubSp ` C ) C_ ( SubGrp ` C ) ) |
52 |
51 43
|
sseldd |
|- ( ph -> ( M ` ( N ` { u } ) ) e. ( SubGrp ` C ) ) |
53 |
51 46
|
sseldd |
|- ( ph -> ( M ` ( N ` { v } ) ) e. ( SubGrp ` C ) ) |
54 |
15 6
|
lspsnid |
|- ( ( C e. LMod /\ ( S ` u ) e. D ) -> ( S ` u ) e. ( L ` { ( S ` u ) } ) ) |
55 |
23 24 54
|
syl2anc |
|- ( ph -> ( S ` u ) e. ( L ` { ( S ` u ) } ) ) |
56 |
1 2 3 4 5 6 7 8 9 13
|
hdmap10 |
|- ( ph -> ( M ` ( N ` { u } ) ) = ( L ` { ( S ` u ) } ) ) |
57 |
55 56
|
eleqtrrd |
|- ( ph -> ( S ` u ) e. ( M ` ( N ` { u } ) ) ) |
58 |
|
eqimss2 |
|- ( ( M ` ( N ` { v } ) ) = ( L ` { s } ) -> ( L ` { s } ) C_ ( M ` ( N ` { v } ) ) ) |
59 |
12 58
|
syl |
|- ( ph -> ( L ` { s } ) C_ ( M ` ( N ` { v } ) ) ) |
60 |
15 38 6 23 46 25
|
lspsnel5 |
|- ( ph -> ( s e. ( M ` ( N ` { v } ) ) <-> ( L ` { s } ) C_ ( M ` ( N ` { v } ) ) ) ) |
61 |
59 60
|
mpbird |
|- ( ph -> s e. ( M ` ( N ` { v } ) ) ) |
62 |
18 47
|
lsmelvali |
|- ( ( ( ( M ` ( N ` { u } ) ) e. ( SubGrp ` C ) /\ ( M ` ( N ` { v } ) ) e. ( SubGrp ` C ) ) /\ ( ( S ` u ) e. ( M ` ( N ` { u } ) ) /\ s e. ( M ` ( N ` { v } ) ) ) ) -> ( ( S ` u ) .+b s ) e. ( ( M ` ( N ` { u } ) ) ( LSSum ` C ) ( M ` ( N ` { v } ) ) ) ) |
63 |
52 53 57 61 62
|
syl22anc |
|- ( ph -> ( ( S ` u ) .+b s ) e. ( ( M ` ( N ` { u } ) ) ( LSSum ` C ) ( M ` ( N ` { v } ) ) ) ) |
64 |
38 6 23 49 63
|
lspsnel5a |
|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) C_ ( ( M ` ( N ` { u } ) ) ( LSSum ` C ) ( M ` ( N ` { v } ) ) ) ) |
65 |
|
eqid |
|- ( LSSum ` U ) = ( LSSum ` U ) |
66 |
1 7 2 39 65 5 47 9 42 45
|
mapdlsm |
|- ( ph -> ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) = ( ( M ` ( N ` { u } ) ) ( LSSum ` C ) ( M ` ( N ` { v } ) ) ) ) |
67 |
64 66
|
sseqtrrd |
|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) C_ ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) ) |
68 |
15 38 6
|
lspsncl |
|- ( ( C e. LMod /\ ( ( S ` u ) .+b s ) e. D ) -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSubSp ` C ) ) |
69 |
23 27 68
|
syl2anc |
|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSubSp ` C ) ) |
70 |
1 7 5 38 9
|
mapdrn2 |
|- ( ph -> ran M = ( LSubSp ` C ) ) |
71 |
69 70
|
eleqtrrd |
|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ran M ) |
72 |
39 65
|
lsmcl |
|- ( ( U e. LMod /\ ( N ` { u } ) e. ( LSubSp ` U ) /\ ( N ` { v } ) e. ( LSubSp ` U ) ) -> ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) e. ( LSubSp ` U ) ) |
73 |
40 42 45 72
|
syl3anc |
|- ( ph -> ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) e. ( LSubSp ` U ) ) |
74 |
1 7 2 39 9 73
|
mapdcl |
|- ( ph -> ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) e. ran M ) |
75 |
1 7 9 71 74
|
mapdcnvordN |
|- ( ph -> ( ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) C_ ( `' M ` ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) ) <-> ( L ` { ( ( S ` u ) .+b s ) } ) C_ ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) ) ) |
76 |
67 75
|
mpbird |
|- ( ph -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) C_ ( `' M ` ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) ) ) |
77 |
3 4 65 40 13 11
|
lsmpr |
|- ( ph -> ( N ` { u , v } ) = ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) |
78 |
1 7 2 39 9 73
|
mapdcnvid1N |
|- ( ph -> ( `' M ` ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) ) = ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) |
79 |
77 78
|
eqtr4d |
|- ( ph -> ( N ` { u , v } ) = ( `' M ` ( M ` ( ( N ` { u } ) ( LSSum ` U ) ( N ` { v } ) ) ) ) ) |
80 |
76 79
|
sseqtrrd |
|- ( ph -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) C_ ( N ` { u , v } ) ) |
81 |
3 19 17 4 20 21 33 13 11 35 37 80
|
lsatfixedN |
|- ( ph -> E. t e. ( ( N ` { v } ) \ { .0. } ) ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) |
82 |
|
simpr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) |
83 |
9
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( K e. HL /\ W e. H ) ) |
84 |
40
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> U e. LMod ) |
85 |
13
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> u e. V ) |
86 |
10
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> s e. ( D \ { Q } ) ) |
87 |
11
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> v e. V ) |
88 |
12
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) |
89 |
14
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> -. u e. ( N ` { v } ) ) |
90 |
|
simplr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> t e. ( ( N ` { v } ) \ { .0. } ) ) |
91 |
1 2 3 4 5 6 7 8 83 86 87 88 85 89 15 16 17 18 90
|
hdmaprnlem4tN |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> t e. V ) |
92 |
3 19
|
lmodvacl |
|- ( ( U e. LMod /\ u e. V /\ t e. V ) -> ( u .+ t ) e. V ) |
93 |
84 85 91 92
|
syl3anc |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( u .+ t ) e. V ) |
94 |
3 39 4
|
lspsncl |
|- ( ( U e. LMod /\ ( u .+ t ) e. V ) -> ( N ` { ( u .+ t ) } ) e. ( LSubSp ` U ) ) |
95 |
84 93 94
|
syl2anc |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( N ` { ( u .+ t ) } ) e. ( LSubSp ` U ) ) |
96 |
1 7 2 39 83 95
|
mapdcnvid1N |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( `' M ` ( M ` ( N ` { ( u .+ t ) } ) ) ) = ( N ` { ( u .+ t ) } ) ) |
97 |
82 96
|
eqtr4d |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( `' M ` ( M ` ( N ` { ( u .+ t ) } ) ) ) ) |
98 |
71
|
ad2antrr |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ran M ) |
99 |
1 7 2 39 83 95
|
mapdcl |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( M ` ( N ` { ( u .+ t ) } ) ) e. ran M ) |
100 |
1 7 83 98 99
|
mapdcnv11N |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( `' M ` ( M ` ( N ` { ( u .+ t ) } ) ) ) <-> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) ) ) |
101 |
97 100
|
mpbid |
|- ( ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) /\ ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) ) -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) ) |
102 |
101
|
ex |
|- ( ( ph /\ t e. ( ( N ` { v } ) \ { .0. } ) ) -> ( ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) ) ) |
103 |
102
|
reximdva |
|- ( ph -> ( E. t e. ( ( N ` { v } ) \ { .0. } ) ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) = ( N ` { ( u .+ t ) } ) -> E. t e. ( ( N ` { v } ) \ { .0. } ) ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) ) ) |
104 |
81 103
|
mpd |
|- ( ph -> E. t e. ( ( N ` { v } ) \ { .0. } ) ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) ) |