| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ply1degltdim.p |
|- P = ( Poly1 ` R ) |
| 2 |
|
ply1degltdim.d |
|- D = ( deg1 ` R ) |
| 3 |
|
ply1degltdim.s |
|- S = ( `' D " ( -oo [,) N ) ) |
| 4 |
|
ply1degltdim.n |
|- ( ph -> N e. NN0 ) |
| 5 |
|
ply1degltdim.r |
|- ( ph -> R e. DivRing ) |
| 6 |
|
ply1degltdim.e |
|- E = ( P |`s S ) |
| 7 |
|
ply1degltdimlem.f |
|- F = ( n e. ( 0 ..^ N ) |-> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) |
| 8 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
| 9 |
4
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> N e. NN0 ) |
| 10 |
5
|
drngringd |
|- ( ph -> R e. Ring ) |
| 11 |
10
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> R e. Ring ) |
| 12 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
| 13 |
|
eqid |
|- ( 0g ` P ) = ( 0g ` P ) |
| 14 |
|
elmapi |
|- ( a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) -> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) ) |
| 15 |
14
|
adantl |
|- ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) ) |
| 16 |
1
|
ply1sca |
|- ( R e. DivRing -> R = ( Scalar ` P ) ) |
| 17 |
5 16
|
syl |
|- ( ph -> R = ( Scalar ` P ) ) |
| 18 |
17
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) ) |
| 19 |
18
|
adantr |
|- ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) ) |
| 20 |
19
|
feq3d |
|- ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> ( a : ( 0 ..^ N ) --> ( Base ` R ) <-> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) ) ) |
| 21 |
15 20
|
mpbird |
|- ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> a : ( 0 ..^ N ) --> ( Base ` R ) ) |
| 22 |
21
|
ad2antrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a : ( 0 ..^ N ) --> ( Base ` R ) ) |
| 23 |
|
simpr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) |
| 24 |
|
ovexd |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( 0 ..^ N ) e. _V ) |
| 25 |
1 5
|
ply1lvec |
|- ( ph -> P e. LVec ) |
| 26 |
25
|
lveclmodd |
|- ( ph -> P e. LMod ) |
| 27 |
1 2 3 4 10
|
ply1degltlss |
|- ( ph -> S e. ( LSubSp ` P ) ) |
| 28 |
|
eqid |
|- ( LSubSp ` P ) = ( LSubSp ` P ) |
| 29 |
28
|
lsssubg |
|- ( ( P e. LMod /\ S e. ( LSubSp ` P ) ) -> S e. ( SubGrp ` P ) ) |
| 30 |
26 27 29
|
syl2anc |
|- ( ph -> S e. ( SubGrp ` P ) ) |
| 31 |
|
subgsubm |
|- ( S e. ( SubGrp ` P ) -> S e. ( SubMnd ` P ) ) |
| 32 |
30 31
|
syl |
|- ( ph -> S e. ( SubMnd ` P ) ) |
| 33 |
32
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> S e. ( SubMnd ` P ) ) |
| 34 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
| 35 |
2 1 34
|
deg1xrf |
|- D : ( Base ` P ) --> RR* |
| 36 |
|
ffn |
|- ( D : ( Base ` P ) --> RR* -> D Fn ( Base ` P ) ) |
| 37 |
35 36
|
mp1i |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> D Fn ( Base ` P ) ) |
| 38 |
|
eqid |
|- ( Scalar ` P ) = ( Scalar ` P ) |
| 39 |
|
eqid |
|- ( .s ` P ) = ( .s ` P ) |
| 40 |
|
eqid |
|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) ) |
| 41 |
26
|
ad2antrr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> P e. LMod ) |
| 42 |
|
simplr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> k e. ( Base ` ( Scalar ` P ) ) ) |
| 43 |
34 28
|
lssss |
|- ( S e. ( LSubSp ` P ) -> S C_ ( Base ` P ) ) |
| 44 |
27 43
|
syl |
|- ( ph -> S C_ ( Base ` P ) ) |
| 45 |
6 34
|
ressbas2 |
|- ( S C_ ( Base ` P ) -> S = ( Base ` E ) ) |
| 46 |
44 45
|
syl |
|- ( ph -> S = ( Base ` E ) ) |
| 47 |
46 44
|
eqsstrrd |
|- ( ph -> ( Base ` E ) C_ ( Base ` P ) ) |
| 48 |
47
|
sselda |
|- ( ( ph /\ x e. ( Base ` E ) ) -> x e. ( Base ` P ) ) |
| 49 |
48
|
adantlr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> x e. ( Base ` P ) ) |
| 50 |
34 38 39 40 41 42 49
|
lmodvscld |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( k ( .s ` P ) x ) e. ( Base ` P ) ) |
| 51 |
|
mnfxr |
|- -oo e. RR* |
| 52 |
51
|
a1i |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> -oo e. RR* ) |
| 53 |
4
|
nn0red |
|- ( ph -> N e. RR ) |
| 54 |
53
|
rexrd |
|- ( ph -> N e. RR* ) |
| 55 |
54
|
ad2antrr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> N e. RR* ) |
| 56 |
35
|
a1i |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> D : ( Base ` P ) --> RR* ) |
| 57 |
56 50
|
ffvelcdmd |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) e. RR* ) |
| 58 |
57
|
mnfled |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> -oo <_ ( D ` ( k ( .s ` P ) x ) ) ) |
| 59 |
56 49
|
ffvelcdmd |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` x ) e. RR* ) |
| 60 |
10
|
ad2antrr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> R e. Ring ) |
| 61 |
18
|
ad2antrr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) ) |
| 62 |
42 61
|
eleqtrrd |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> k e. ( Base ` R ) ) |
| 63 |
1 2 60 34 8 39 62 49
|
deg1vscale |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) <_ ( D ` x ) ) |
| 64 |
|
simpll |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ph ) |
| 65 |
|
simpr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> x e. ( Base ` E ) ) |
| 66 |
46
|
ad2antrr |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> S = ( Base ` E ) ) |
| 67 |
65 66
|
eleqtrrd |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> x e. S ) |
| 68 |
51
|
a1i |
|- ( ( ph /\ x e. S ) -> -oo e. RR* ) |
| 69 |
54
|
adantr |
|- ( ( ph /\ x e. S ) -> N e. RR* ) |
| 70 |
35 36
|
mp1i |
|- ( ( ph /\ x e. S ) -> D Fn ( Base ` P ) ) |
| 71 |
|
simpr |
|- ( ( ph /\ x e. S ) -> x e. S ) |
| 72 |
71 3
|
eleqtrdi |
|- ( ( ph /\ x e. S ) -> x e. ( `' D " ( -oo [,) N ) ) ) |
| 73 |
|
elpreima |
|- ( D Fn ( Base ` P ) -> ( x e. ( `' D " ( -oo [,) N ) ) <-> ( x e. ( Base ` P ) /\ ( D ` x ) e. ( -oo [,) N ) ) ) ) |
| 74 |
73
|
simplbda |
|- ( ( D Fn ( Base ` P ) /\ x e. ( `' D " ( -oo [,) N ) ) ) -> ( D ` x ) e. ( -oo [,) N ) ) |
| 75 |
70 72 74
|
syl2anc |
|- ( ( ph /\ x e. S ) -> ( D ` x ) e. ( -oo [,) N ) ) |
| 76 |
|
elico1 |
|- ( ( -oo e. RR* /\ N e. RR* ) -> ( ( D ` x ) e. ( -oo [,) N ) <-> ( ( D ` x ) e. RR* /\ -oo <_ ( D ` x ) /\ ( D ` x ) < N ) ) ) |
| 77 |
76
|
biimpa |
|- ( ( ( -oo e. RR* /\ N e. RR* ) /\ ( D ` x ) e. ( -oo [,) N ) ) -> ( ( D ` x ) e. RR* /\ -oo <_ ( D ` x ) /\ ( D ` x ) < N ) ) |
| 78 |
77
|
simp3d |
|- ( ( ( -oo e. RR* /\ N e. RR* ) /\ ( D ` x ) e. ( -oo [,) N ) ) -> ( D ` x ) < N ) |
| 79 |
68 69 75 78
|
syl21anc |
|- ( ( ph /\ x e. S ) -> ( D ` x ) < N ) |
| 80 |
64 67 79
|
syl2anc |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` x ) < N ) |
| 81 |
57 59 55 63 80
|
xrlelttrd |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) < N ) |
| 82 |
52 55 57 58 81
|
elicod |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) e. ( -oo [,) N ) ) |
| 83 |
37 50 82
|
elpreimad |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( k ( .s ` P ) x ) e. ( `' D " ( -oo [,) N ) ) ) |
| 84 |
83 3
|
eleqtrrdi |
|- ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( k ( .s ` P ) x ) e. S ) |
| 85 |
84
|
anasss |
|- ( ( ph /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ x e. ( Base ` E ) ) ) -> ( k ( .s ` P ) x ) e. S ) |
| 86 |
85
|
ad5ant15 |
|- ( ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ x e. ( Base ` E ) ) ) -> ( k ( .s ` P ) x ) e. S ) |
| 87 |
15
|
ad2antrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) ) |
| 88 |
35 36
|
mp1i |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> D Fn ( Base ` P ) ) |
| 89 |
|
eqid |
|- ( mulGrp ` P ) = ( mulGrp ` P ) |
| 90 |
89 34
|
mgpbas |
|- ( Base ` P ) = ( Base ` ( mulGrp ` P ) ) |
| 91 |
|
eqid |
|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) ) |
| 92 |
1
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
| 93 |
89
|
ringmgp |
|- ( P e. Ring -> ( mulGrp ` P ) e. Mnd ) |
| 94 |
10 92 93
|
3syl |
|- ( ph -> ( mulGrp ` P ) e. Mnd ) |
| 95 |
94
|
adantr |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( mulGrp ` P ) e. Mnd ) |
| 96 |
|
elfzonn0 |
|- ( n e. ( 0 ..^ N ) -> n e. NN0 ) |
| 97 |
96
|
adantl |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> n e. NN0 ) |
| 98 |
|
eqid |
|- ( var1 ` R ) = ( var1 ` R ) |
| 99 |
98 1 34
|
vr1cl |
|- ( R e. Ring -> ( var1 ` R ) e. ( Base ` P ) ) |
| 100 |
10 99
|
syl |
|- ( ph -> ( var1 ` R ) e. ( Base ` P ) ) |
| 101 |
100
|
adantr |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( var1 ` R ) e. ( Base ` P ) ) |
| 102 |
90 91 95 97 101
|
mulgnn0cld |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) ) |
| 103 |
51
|
a1i |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> -oo e. RR* ) |
| 104 |
54
|
adantr |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> N e. RR* ) |
| 105 |
2 1 34
|
deg1xrcl |
|- ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* ) |
| 106 |
102 105
|
syl |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* ) |
| 107 |
106
|
mnfled |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> -oo <_ ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 108 |
96
|
nn0red |
|- ( n e. ( 0 ..^ N ) -> n e. RR ) |
| 109 |
108
|
rexrd |
|- ( n e. ( 0 ..^ N ) -> n e. RR* ) |
| 110 |
109
|
adantl |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> n e. RR* ) |
| 111 |
2 1 98 89 91
|
deg1pwle |
|- ( ( R e. Ring /\ n e. NN0 ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ n ) |
| 112 |
10 96 111
|
syl2an |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ n ) |
| 113 |
|
elfzolt2 |
|- ( n e. ( 0 ..^ N ) -> n < N ) |
| 114 |
113
|
adantl |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> n < N ) |
| 115 |
106 110 104 112 114
|
xrlelttrd |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) < N ) |
| 116 |
103 104 106 107 115
|
elicod |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( -oo [,) N ) ) |
| 117 |
88 102 116
|
elpreimad |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( `' D " ( -oo [,) N ) ) ) |
| 118 |
117 3
|
eleqtrrdi |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. S ) |
| 119 |
46
|
adantr |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> S = ( Base ` E ) ) |
| 120 |
118 119
|
eleqtrd |
|- ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) ) |
| 121 |
120 7
|
fmptd |
|- ( ph -> F : ( 0 ..^ N ) --> ( Base ` E ) ) |
| 122 |
121
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> F : ( 0 ..^ N ) --> ( Base ` E ) ) |
| 123 |
|
inidm |
|- ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) = ( 0 ..^ N ) |
| 124 |
86 87 122 24 24 123
|
off |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( a oF ( .s ` P ) F ) : ( 0 ..^ N ) --> S ) |
| 125 |
24 33 124 6
|
gsumsubm |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( P gsum ( a oF ( .s ` P ) F ) ) = ( E gsum ( a oF ( .s ` P ) F ) ) ) |
| 126 |
|
ringmnd |
|- ( P e. Ring -> P e. Mnd ) |
| 127 |
10 92 126
|
3syl |
|- ( ph -> P e. Mnd ) |
| 128 |
35 36
|
mp1i |
|- ( ph -> D Fn ( Base ` P ) ) |
| 129 |
34 13
|
mndidcl |
|- ( P e. Mnd -> ( 0g ` P ) e. ( Base ` P ) ) |
| 130 |
127 129
|
syl |
|- ( ph -> ( 0g ` P ) e. ( Base ` P ) ) |
| 131 |
51
|
a1i |
|- ( ph -> -oo e. RR* ) |
| 132 |
2 1 34
|
deg1xrcl |
|- ( ( 0g ` P ) e. ( Base ` P ) -> ( D ` ( 0g ` P ) ) e. RR* ) |
| 133 |
130 132
|
syl |
|- ( ph -> ( D ` ( 0g ` P ) ) e. RR* ) |
| 134 |
133
|
mnfled |
|- ( ph -> -oo <_ ( D ` ( 0g ` P ) ) ) |
| 135 |
2 1 13
|
deg1z |
|- ( R e. Ring -> ( D ` ( 0g ` P ) ) = -oo ) |
| 136 |
10 135
|
syl |
|- ( ph -> ( D ` ( 0g ` P ) ) = -oo ) |
| 137 |
53
|
mnfltd |
|- ( ph -> -oo < N ) |
| 138 |
136 137
|
eqbrtrd |
|- ( ph -> ( D ` ( 0g ` P ) ) < N ) |
| 139 |
131 54 133 134 138
|
elicod |
|- ( ph -> ( D ` ( 0g ` P ) ) e. ( -oo [,) N ) ) |
| 140 |
128 130 139
|
elpreimad |
|- ( ph -> ( 0g ` P ) e. ( `' D " ( -oo [,) N ) ) ) |
| 141 |
140 3
|
eleqtrrdi |
|- ( ph -> ( 0g ` P ) e. S ) |
| 142 |
6 34 13
|
ress0g |
|- ( ( P e. Mnd /\ ( 0g ` P ) e. S /\ S C_ ( Base ` P ) ) -> ( 0g ` P ) = ( 0g ` E ) ) |
| 143 |
127 141 44 142
|
syl3anc |
|- ( ph -> ( 0g ` P ) = ( 0g ` E ) ) |
| 144 |
143
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( 0g ` P ) = ( 0g ` E ) ) |
| 145 |
23 125 144
|
3eqtr4d |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( P gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` P ) ) |
| 146 |
1 8 9 11 7 12 13 22 145
|
ply1gsumz |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` R ) } ) ) |
| 147 |
17
|
fveq2d |
|- ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) ) |
| 148 |
147
|
sneqd |
|- ( ph -> { ( 0g ` R ) } = { ( 0g ` ( Scalar ` P ) ) } ) |
| 149 |
148
|
xpeq2d |
|- ( ph -> ( ( 0 ..^ N ) X. { ( 0g ` R ) } ) = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) |
| 150 |
149
|
ad3antrrr |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( ( 0 ..^ N ) X. { ( 0g ` R ) } ) = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) |
| 151 |
146 150
|
eqtrd |
|- ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) |
| 152 |
151
|
expl |
|- ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) ) |
| 153 |
152
|
ralrimiva |
|- ( ph -> A. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) ) |
| 154 |
118 7
|
fmptd |
|- ( ph -> F : ( 0 ..^ N ) --> S ) |
| 155 |
154
|
frnd |
|- ( ph -> ran F C_ S ) |
| 156 |
|
eqid |
|- ( LSpan ` P ) = ( LSpan ` P ) |
| 157 |
28 156
|
lspssp |
|- ( ( P e. LMod /\ S e. ( LSubSp ` P ) /\ ran F C_ S ) -> ( ( LSpan ` P ) ` ran F ) C_ S ) |
| 158 |
26 27 155 157
|
syl3anc |
|- ( ph -> ( ( LSpan ` P ) ` ran F ) C_ S ) |
| 159 |
|
breq1 |
|- ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( a finSupp ( 0g ` ( Scalar ` P ) ) <-> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) ) ) |
| 160 |
|
oveq1 |
|- ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( a oF ( .s ` P ) F ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) |
| 161 |
160
|
oveq2d |
|- ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( P gsum ( a oF ( .s ` P ) F ) ) = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) |
| 162 |
161
|
eqeq2d |
|- ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( x = ( P gsum ( a oF ( .s ` P ) F ) ) <-> x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) ) |
| 163 |
159 162
|
anbi12d |
|- ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) <-> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) ) ) |
| 164 |
|
fvexd |
|- ( ( ph /\ x e. S ) -> ( Base ` ( Scalar ` P ) ) e. _V ) |
| 165 |
|
ovexd |
|- ( ( ph /\ x e. S ) -> ( 0 ..^ N ) e. _V ) |
| 166 |
44
|
sselda |
|- ( ( ph /\ x e. S ) -> x e. ( Base ` P ) ) |
| 167 |
|
eqid |
|- ( coe1 ` x ) = ( coe1 ` x ) |
| 168 |
167 34 1 8
|
coe1f |
|- ( x e. ( Base ` P ) -> ( coe1 ` x ) : NN0 --> ( Base ` R ) ) |
| 169 |
166 168
|
syl |
|- ( ( ph /\ x e. S ) -> ( coe1 ` x ) : NN0 --> ( Base ` R ) ) |
| 170 |
18
|
adantr |
|- ( ( ph /\ x e. S ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) ) |
| 171 |
170
|
feq3d |
|- ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) : NN0 --> ( Base ` R ) <-> ( coe1 ` x ) : NN0 --> ( Base ` ( Scalar ` P ) ) ) ) |
| 172 |
169 171
|
mpbid |
|- ( ( ph /\ x e. S ) -> ( coe1 ` x ) : NN0 --> ( Base ` ( Scalar ` P ) ) ) |
| 173 |
|
fzo0ssnn0 |
|- ( 0 ..^ N ) C_ NN0 |
| 174 |
173
|
a1i |
|- ( ( ph /\ x e. S ) -> ( 0 ..^ N ) C_ NN0 ) |
| 175 |
172 174
|
fssresd |
|- ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) ) |
| 176 |
164 165 175
|
elmapdd |
|- ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) |
| 177 |
169
|
ffund |
|- ( ( ph /\ x e. S ) -> Fun ( coe1 ` x ) ) |
| 178 |
|
fzofi |
|- ( 0 ..^ N ) e. Fin |
| 179 |
178
|
a1i |
|- ( ( ph /\ x e. S ) -> ( 0 ..^ N ) e. Fin ) |
| 180 |
|
fvexd |
|- ( ( ph /\ x e. S ) -> ( 0g ` ( Scalar ` P ) ) e. _V ) |
| 181 |
177 179 180
|
resfifsupp |
|- ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) ) |
| 182 |
|
ringcmn |
|- ( P e. Ring -> P e. CMnd ) |
| 183 |
10 92 182
|
3syl |
|- ( ph -> P e. CMnd ) |
| 184 |
183
|
adantr |
|- ( ( ph /\ x e. S ) -> P e. CMnd ) |
| 185 |
|
nn0ex |
|- NN0 e. _V |
| 186 |
185
|
a1i |
|- ( ( ph /\ x e. S ) -> NN0 e. _V ) |
| 187 |
26
|
ad2antrr |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> P e. LMod ) |
| 188 |
172
|
ffvelcdmda |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( ( coe1 ` x ) ` i ) e. ( Base ` ( Scalar ` P ) ) ) |
| 189 |
10
|
ad2antrr |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> R e. Ring ) |
| 190 |
189 92 93
|
3syl |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( mulGrp ` P ) e. Mnd ) |
| 191 |
|
simpr |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> i e. NN0 ) |
| 192 |
189 99
|
syl |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( var1 ` R ) e. ( Base ` P ) ) |
| 193 |
90 91 190 191 192
|
mulgnn0cld |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) ) |
| 194 |
34 38 39 40 187 188 193
|
lmodvscld |
|- ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( Base ` P ) ) |
| 195 |
|
eqid |
|- ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 196 |
194 195
|
fmptd |
|- ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) : NN0 --> ( Base ` P ) ) |
| 197 |
|
nfv |
|- F/ i ( ph /\ x e. S ) |
| 198 |
197 194 195
|
fnmptd |
|- ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) Fn NN0 ) |
| 199 |
|
fveq2 |
|- ( i = j -> ( ( coe1 ` x ) ` i ) = ( ( coe1 ` x ) ` j ) ) |
| 200 |
|
oveq1 |
|- ( i = j -> ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) |
| 201 |
199 200
|
oveq12d |
|- ( i = j -> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 202 |
|
simplr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> j e. NN0 ) |
| 203 |
|
ovexd |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. _V ) |
| 204 |
195 201 202 203
|
fvmptd3 |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 205 |
166
|
ad2antrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> x e. ( Base ` P ) ) |
| 206 |
|
icossxr |
|- ( -oo [,) N ) C_ RR* |
| 207 |
206 75
|
sselid |
|- ( ( ph /\ x e. S ) -> ( D ` x ) e. RR* ) |
| 208 |
207
|
ad2antrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( D ` x ) e. RR* ) |
| 209 |
54
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> N e. RR* ) |
| 210 |
202
|
nn0red |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> j e. RR ) |
| 211 |
210
|
rexrd |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> j e. RR* ) |
| 212 |
79
|
ad2antrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( D ` x ) < N ) |
| 213 |
|
simpr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> N <_ j ) |
| 214 |
208 209 211 212 213
|
xrltletrd |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( D ` x ) < j ) |
| 215 |
2 1 34 12 167
|
deg1lt |
|- ( ( x e. ( Base ` P ) /\ j e. NN0 /\ ( D ` x ) < j ) -> ( ( coe1 ` x ) ` j ) = ( 0g ` R ) ) |
| 216 |
205 202 214 215
|
syl3anc |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( coe1 ` x ) ` j ) = ( 0g ` R ) ) |
| 217 |
216
|
oveq1d |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( 0g ` R ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 218 |
147
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) ) |
| 219 |
218
|
oveq1d |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( 0g ` R ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 220 |
26
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> P e. LMod ) |
| 221 |
94
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( mulGrp ` P ) e. Mnd ) |
| 222 |
100
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( var1 ` R ) e. ( Base ` P ) ) |
| 223 |
90 91 221 202 222
|
mulgnn0cld |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) ) |
| 224 |
|
eqid |
|- ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) ) |
| 225 |
34 38 39 224 13
|
lmod0vs |
|- ( ( P e. LMod /\ ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) ) |
| 226 |
220 223 225
|
syl2anc |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) ) |
| 227 |
219 226
|
eqtrd |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( 0g ` R ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) ) |
| 228 |
204 217 227
|
3eqtrd |
|- ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) = ( 0g ` P ) ) |
| 229 |
4
|
nn0zd |
|- ( ph -> N e. ZZ ) |
| 230 |
229
|
adantr |
|- ( ( ph /\ x e. S ) -> N e. ZZ ) |
| 231 |
198 228 230
|
suppssnn0 |
|- ( ( ph /\ x e. S ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) supp ( 0g ` P ) ) C_ ( 0 ..^ N ) ) |
| 232 |
186
|
mptexd |
|- ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) e. _V ) |
| 233 |
198
|
fnfund |
|- ( ( ph /\ x e. S ) -> Fun ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) |
| 234 |
|
fvexd |
|- ( ( ph /\ x e. S ) -> ( 0g ` P ) e. _V ) |
| 235 |
|
suppssfifsupp |
|- ( ( ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) e. _V /\ Fun ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) /\ ( 0g ` P ) e. _V ) /\ ( ( 0 ..^ N ) e. Fin /\ ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) supp ( 0g ` P ) ) C_ ( 0 ..^ N ) ) ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) finSupp ( 0g ` P ) ) |
| 236 |
232 233 234 179 231 235
|
syl32anc |
|- ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) finSupp ( 0g ` P ) ) |
| 237 |
34 13 184 186 196 231 236
|
gsumres |
|- ( ( ph /\ x e. S ) -> ( P gsum ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) ) = ( P gsum ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
| 238 |
|
fvexd |
|- ( ( ph /\ x e. S ) -> ( coe1 ` x ) e. _V ) |
| 239 |
|
ovexd |
|- ( ph -> ( 0 ..^ N ) e. _V ) |
| 240 |
154 239
|
fexd |
|- ( ph -> F e. _V ) |
| 241 |
240
|
adantr |
|- ( ( ph /\ x e. S ) -> F e. _V ) |
| 242 |
|
offres |
|- ( ( ( coe1 ` x ) e. _V /\ F e. _V ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) ( F |` ( 0 ..^ N ) ) ) ) |
| 243 |
238 241 242
|
syl2anc |
|- ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) ( F |` ( 0 ..^ N ) ) ) ) |
| 244 |
169
|
ffnd |
|- ( ( ph /\ x e. S ) -> ( coe1 ` x ) Fn NN0 ) |
| 245 |
154
|
ffnd |
|- ( ph -> F Fn ( 0 ..^ N ) ) |
| 246 |
245
|
adantr |
|- ( ( ph /\ x e. S ) -> F Fn ( 0 ..^ N ) ) |
| 247 |
|
sseqin2 |
|- ( ( 0 ..^ N ) C_ NN0 <-> ( NN0 i^i ( 0 ..^ N ) ) = ( 0 ..^ N ) ) |
| 248 |
173 247
|
mpbi |
|- ( NN0 i^i ( 0 ..^ N ) ) = ( 0 ..^ N ) |
| 249 |
|
eqidd |
|- ( ( ( ph /\ x e. S ) /\ j e. NN0 ) -> ( ( coe1 ` x ) ` j ) = ( ( coe1 ` x ) ` j ) ) |
| 250 |
|
oveq1 |
|- ( n = j -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) |
| 251 |
|
simpr |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) ) |
| 252 |
|
ovexd |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. _V ) |
| 253 |
7 250 251 252
|
fvmptd3 |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( F ` j ) = ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) |
| 254 |
244 246 186 165 248 249 253
|
ofval |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 255 |
173 251
|
sselid |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> j e. NN0 ) |
| 256 |
|
ovexd |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. _V ) |
| 257 |
195 201 255 256
|
fvmptd3 |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
| 258 |
254 257
|
eqtr4d |
|- ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) ) |
| 259 |
258
|
ralrimiva |
|- ( ( ph /\ x e. S ) -> A. j e. ( 0 ..^ N ) ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) ) |
| 260 |
244 246 186 165 248
|
offn |
|- ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) oF ( .s ` P ) F ) Fn ( 0 ..^ N ) ) |
| 261 |
|
ssidd |
|- ( ( ph /\ x e. S ) -> ( 0 ..^ N ) C_ ( 0 ..^ N ) ) |
| 262 |
|
fvreseq0 |
|- ( ( ( ( ( coe1 ` x ) oF ( .s ` P ) F ) Fn ( 0 ..^ N ) /\ ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) Fn NN0 ) /\ ( ( 0 ..^ N ) C_ ( 0 ..^ N ) /\ ( 0 ..^ N ) C_ NN0 ) ) -> ( ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) <-> A. j e. ( 0 ..^ N ) ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) ) ) |
| 263 |
260 198 261 174 262
|
syl22anc |
|- ( ( ph /\ x e. S ) -> ( ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) <-> A. j e. ( 0 ..^ N ) ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) ) ) |
| 264 |
259 263
|
mpbird |
|- ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) ) |
| 265 |
|
fnresdm |
|- ( F Fn ( 0 ..^ N ) -> ( F |` ( 0 ..^ N ) ) = F ) |
| 266 |
245 265
|
syl |
|- ( ph -> ( F |` ( 0 ..^ N ) ) = F ) |
| 267 |
266
|
adantr |
|- ( ( ph /\ x e. S ) -> ( F |` ( 0 ..^ N ) ) = F ) |
| 268 |
267
|
oveq2d |
|- ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) ( F |` ( 0 ..^ N ) ) ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) |
| 269 |
243 264 268
|
3eqtr3rd |
|- ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) ) |
| 270 |
269
|
oveq2d |
|- ( ( ph /\ x e. S ) -> ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) = ( P gsum ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) ) ) |
| 271 |
10
|
adantr |
|- ( ( ph /\ x e. S ) -> R e. Ring ) |
| 272 |
1 98 34 39 89 91 167
|
ply1coe |
|- ( ( R e. Ring /\ x e. ( Base ` P ) ) -> x = ( P gsum ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
| 273 |
271 166 272
|
syl2anc |
|- ( ( ph /\ x e. S ) -> x = ( P gsum ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
| 274 |
237 270 273
|
3eqtr4rd |
|- ( ( ph /\ x e. S ) -> x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) |
| 275 |
181 274
|
jca |
|- ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) ) |
| 276 |
163 176 275
|
rspcedvdw |
|- ( ( ph /\ x e. S ) -> E. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) ) |
| 277 |
102 7
|
fmptd |
|- ( ph -> F : ( 0 ..^ N ) --> ( Base ` P ) ) |
| 278 |
156 34 40 38 224 39 277 26 239
|
ellspd |
|- ( ph -> ( x e. ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) <-> E. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) ) ) |
| 279 |
278
|
adantr |
|- ( ( ph /\ x e. S ) -> ( x e. ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) <-> E. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) ) ) |
| 280 |
276 279
|
mpbird |
|- ( ( ph /\ x e. S ) -> x e. ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) ) |
| 281 |
|
imadmrn |
|- ( F " dom F ) = ran F |
| 282 |
154
|
fdmd |
|- ( ph -> dom F = ( 0 ..^ N ) ) |
| 283 |
282
|
imaeq2d |
|- ( ph -> ( F " dom F ) = ( F " ( 0 ..^ N ) ) ) |
| 284 |
281 283
|
eqtr3id |
|- ( ph -> ran F = ( F " ( 0 ..^ N ) ) ) |
| 285 |
284
|
fveq2d |
|- ( ph -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) ) |
| 286 |
285
|
adantr |
|- ( ( ph /\ x e. S ) -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) ) |
| 287 |
280 286
|
eleqtrrd |
|- ( ( ph /\ x e. S ) -> x e. ( ( LSpan ` P ) ` ran F ) ) |
| 288 |
158 287
|
eqelssd |
|- ( ph -> ( ( LSpan ` P ) ` ran F ) = S ) |
| 289 |
|
eqid |
|- ( LSpan ` E ) = ( LSpan ` E ) |
| 290 |
6 156 289 28
|
lsslsp |
|- ( ( P e. LMod /\ S e. ( LSubSp ` P ) /\ ran F C_ S ) -> ( ( LSpan ` E ) ` ran F ) = ( ( LSpan ` P ) ` ran F ) ) |
| 291 |
290
|
eqcomd |
|- ( ( P e. LMod /\ S e. ( LSubSp ` P ) /\ ran F C_ S ) -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` E ) ` ran F ) ) |
| 292 |
26 27 155 291
|
syl3anc |
|- ( ph -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` E ) ` ran F ) ) |
| 293 |
288 292 46
|
3eqtr3d |
|- ( ph -> ( ( LSpan ` E ) ` ran F ) = ( Base ` E ) ) |
| 294 |
|
eqid |
|- ( Base ` E ) = ( Base ` E ) |
| 295 |
2
|
fvexi |
|- D e. _V |
| 296 |
|
cnvexg |
|- ( D e. _V -> `' D e. _V ) |
| 297 |
|
imaexg |
|- ( `' D e. _V -> ( `' D " ( -oo [,) N ) ) e. _V ) |
| 298 |
295 296 297
|
mp2b |
|- ( `' D " ( -oo [,) N ) ) e. _V |
| 299 |
3 298
|
eqeltri |
|- S e. _V |
| 300 |
6 38
|
resssca |
|- ( S e. _V -> ( Scalar ` P ) = ( Scalar ` E ) ) |
| 301 |
299 300
|
ax-mp |
|- ( Scalar ` P ) = ( Scalar ` E ) |
| 302 |
301
|
fveq2i |
|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` E ) ) |
| 303 |
|
eqid |
|- ( Scalar ` E ) = ( Scalar ` E ) |
| 304 |
6 39
|
ressvsca |
|- ( S e. _V -> ( .s ` P ) = ( .s ` E ) ) |
| 305 |
299 304
|
ax-mp |
|- ( .s ` P ) = ( .s ` E ) |
| 306 |
|
eqid |
|- ( 0g ` E ) = ( 0g ` E ) |
| 307 |
301
|
fveq2i |
|- ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` E ) ) |
| 308 |
|
eqid |
|- ( LBasis ` E ) = ( LBasis ` E ) |
| 309 |
6 28
|
lsslvec |
|- ( ( P e. LVec /\ S e. ( LSubSp ` P ) ) -> E e. LVec ) |
| 310 |
25 27 309
|
syl2anc |
|- ( ph -> E e. LVec ) |
| 311 |
310
|
lveclmodd |
|- ( ph -> E e. LMod ) |
| 312 |
17 5
|
eqeltrrd |
|- ( ph -> ( Scalar ` P ) e. DivRing ) |
| 313 |
|
drngnzr |
|- ( ( Scalar ` P ) e. DivRing -> ( Scalar ` P ) e. NzRing ) |
| 314 |
312 313
|
syl |
|- ( ph -> ( Scalar ` P ) e. NzRing ) |
| 315 |
301 314
|
eqeltrrid |
|- ( ph -> ( Scalar ` E ) e. NzRing ) |
| 316 |
120
|
ralrimiva |
|- ( ph -> A. n e. ( 0 ..^ N ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) ) |
| 317 |
|
drngnzr |
|- ( R e. DivRing -> R e. NzRing ) |
| 318 |
5 317
|
syl |
|- ( ph -> R e. NzRing ) |
| 319 |
318
|
ad2antrr |
|- ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> R e. NzRing ) |
| 320 |
97
|
adantr |
|- ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> n e. NN0 ) |
| 321 |
|
elfzonn0 |
|- ( i e. ( 0 ..^ N ) -> i e. NN0 ) |
| 322 |
321
|
adantl |
|- ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> i e. NN0 ) |
| 323 |
1 98 91 319 320 322
|
ply1moneq |
|- ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) <-> n = i ) ) |
| 324 |
323
|
biimpd |
|- ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) ) |
| 325 |
324
|
anasss |
|- ( ( ph /\ ( n e. ( 0 ..^ N ) /\ i e. ( 0 ..^ N ) ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) ) |
| 326 |
325
|
ralrimivva |
|- ( ph -> A. n e. ( 0 ..^ N ) A. i e. ( 0 ..^ N ) ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) ) |
| 327 |
|
oveq1 |
|- ( n = i -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) |
| 328 |
7 327
|
f1mpt |
|- ( F : ( 0 ..^ N ) -1-1-> ( Base ` E ) <-> ( A. n e. ( 0 ..^ N ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) /\ A. n e. ( 0 ..^ N ) A. i e. ( 0 ..^ N ) ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) ) ) |
| 329 |
316 326 328
|
sylanbrc |
|- ( ph -> F : ( 0 ..^ N ) -1-1-> ( Base ` E ) ) |
| 330 |
294 302 303 305 306 307 308 289 311 315 239 329
|
islbs5 |
|- ( ph -> ( ran F e. ( LBasis ` E ) <-> ( A. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) /\ ( ( LSpan ` E ) ` ran F ) = ( Base ` E ) ) ) ) |
| 331 |
153 293 330
|
mpbir2and |
|- ( ph -> ran F e. ( LBasis ` E ) ) |