Step |
Hyp |
Ref |
Expression |
1 |
|
evlslem3.p |
|- P = ( I mPoly R ) |
2 |
|
evlslem3.b |
|- B = ( Base ` P ) |
3 |
|
evlslem3.c |
|- C = ( Base ` S ) |
4 |
|
evlslem3.k |
|- K = ( Base ` R ) |
5 |
|
evlslem3.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
6 |
|
evlslem3.t |
|- T = ( mulGrp ` S ) |
7 |
|
evlslem3.x |
|- .^ = ( .g ` T ) |
8 |
|
evlslem3.m |
|- .x. = ( .r ` S ) |
9 |
|
evlslem3.v |
|- V = ( I mVar R ) |
10 |
|
evlslem3.e |
|- E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
11 |
|
evlslem3.i |
|- ( ph -> I e. W ) |
12 |
|
evlslem3.r |
|- ( ph -> R e. CRing ) |
13 |
|
evlslem3.s |
|- ( ph -> S e. CRing ) |
14 |
|
evlslem3.f |
|- ( ph -> F e. ( R RingHom S ) ) |
15 |
|
evlslem3.g |
|- ( ph -> G : I --> C ) |
16 |
|
evlslem3.z |
|- .0. = ( 0g ` R ) |
17 |
|
evlslem3.a |
|- ( ph -> A e. D ) |
18 |
|
evlslem3.q |
|- ( ph -> H e. K ) |
19 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
20 |
12 19
|
syl |
|- ( ph -> R e. Ring ) |
21 |
1 5 16 4 11 20 2 18 17
|
mplmon2cl |
|- ( ph -> ( x e. D |-> if ( x = A , H , .0. ) ) e. B ) |
22 |
|
fveq1 |
|- ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( p ` b ) = ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) |
23 |
22
|
fveq2d |
|- ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( F ` ( p ` b ) ) = ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) ) |
24 |
23
|
oveq1d |
|- ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
25 |
24
|
mpteq2dv |
|- ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
26 |
25
|
oveq2d |
|- ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
27 |
|
ovex |
|- ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V |
28 |
26 10 27
|
fvmpt |
|- ( ( x e. D |-> if ( x = A , H , .0. ) ) e. B -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
29 |
21 28
|
syl |
|- ( ph -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
30 |
|
eqid |
|- ( x e. D |-> if ( x = A , H , .0. ) ) = ( x e. D |-> if ( x = A , H , .0. ) ) |
31 |
|
eqeq1 |
|- ( x = b -> ( x = A <-> b = A ) ) |
32 |
31
|
ifbid |
|- ( x = b -> if ( x = A , H , .0. ) = if ( b = A , H , .0. ) ) |
33 |
|
simpr |
|- ( ( ph /\ b e. D ) -> b e. D ) |
34 |
16
|
fvexi |
|- .0. e. _V |
35 |
34
|
a1i |
|- ( ph -> .0. e. _V ) |
36 |
|
ifexg |
|- ( ( H e. K /\ .0. e. _V ) -> if ( b = A , H , .0. ) e. _V ) |
37 |
18 35 36
|
syl2anc |
|- ( ph -> if ( b = A , H , .0. ) e. _V ) |
38 |
37
|
adantr |
|- ( ( ph /\ b e. D ) -> if ( b = A , H , .0. ) e. _V ) |
39 |
30 32 33 38
|
fvmptd3 |
|- ( ( ph /\ b e. D ) -> ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) = if ( b = A , H , .0. ) ) |
40 |
39
|
fveq2d |
|- ( ( ph /\ b e. D ) -> ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) = ( F ` if ( b = A , H , .0. ) ) ) |
41 |
40
|
oveq1d |
|- ( ( ph /\ b e. D ) -> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
42 |
41
|
mpteq2dva |
|- ( ph -> ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
43 |
42
|
oveq2d |
|- ( ph -> ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
44 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
45 |
|
crngring |
|- ( S e. CRing -> S e. Ring ) |
46 |
13 45
|
syl |
|- ( ph -> S e. Ring ) |
47 |
|
ringmnd |
|- ( S e. Ring -> S e. Mnd ) |
48 |
46 47
|
syl |
|- ( ph -> S e. Mnd ) |
49 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
50 |
5 49
|
rabex2 |
|- D e. _V |
51 |
50
|
a1i |
|- ( ph -> D e. _V ) |
52 |
46
|
adantr |
|- ( ( ph /\ b e. D ) -> S e. Ring ) |
53 |
4 3
|
rhmf |
|- ( F e. ( R RingHom S ) -> F : K --> C ) |
54 |
14 53
|
syl |
|- ( ph -> F : K --> C ) |
55 |
4 16
|
ring0cl |
|- ( R e. Ring -> .0. e. K ) |
56 |
20 55
|
syl |
|- ( ph -> .0. e. K ) |
57 |
18 56
|
ifcld |
|- ( ph -> if ( b = A , H , .0. ) e. K ) |
58 |
54 57
|
ffvelrnd |
|- ( ph -> ( F ` if ( b = A , H , .0. ) ) e. C ) |
59 |
58
|
adantr |
|- ( ( ph /\ b e. D ) -> ( F ` if ( b = A , H , .0. ) ) e. C ) |
60 |
6 3
|
mgpbas |
|- C = ( Base ` T ) |
61 |
|
eqid |
|- ( 0g ` T ) = ( 0g ` T ) |
62 |
6
|
crngmgp |
|- ( S e. CRing -> T e. CMnd ) |
63 |
13 62
|
syl |
|- ( ph -> T e. CMnd ) |
64 |
63
|
adantr |
|- ( ( ph /\ b e. D ) -> T e. CMnd ) |
65 |
11
|
adantr |
|- ( ( ph /\ b e. D ) -> I e. W ) |
66 |
|
cmnmnd |
|- ( T e. CMnd -> T e. Mnd ) |
67 |
63 66
|
syl |
|- ( ph -> T e. Mnd ) |
68 |
67
|
ad2antrr |
|- ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> T e. Mnd ) |
69 |
|
simprl |
|- ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> y e. NN0 ) |
70 |
|
simprr |
|- ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> z e. C ) |
71 |
60 7
|
mulgnn0cl |
|- ( ( T e. Mnd /\ y e. NN0 /\ z e. C ) -> ( y .^ z ) e. C ) |
72 |
68 69 70 71
|
syl3anc |
|- ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> ( y .^ z ) e. C ) |
73 |
5
|
psrbagf |
|- ( b e. D -> b : I --> NN0 ) |
74 |
73
|
adantl |
|- ( ( ph /\ b e. D ) -> b : I --> NN0 ) |
75 |
15
|
adantr |
|- ( ( ph /\ b e. D ) -> G : I --> C ) |
76 |
|
inidm |
|- ( I i^i I ) = I |
77 |
72 74 75 65 65 76
|
off |
|- ( ( ph /\ b e. D ) -> ( b oF .^ G ) : I --> C ) |
78 |
|
ovex |
|- ( b oF .^ G ) e. _V |
79 |
78
|
a1i |
|- ( ( ph /\ b e. D ) -> ( b oF .^ G ) e. _V ) |
80 |
77
|
ffund |
|- ( ( ph /\ b e. D ) -> Fun ( b oF .^ G ) ) |
81 |
|
fvexd |
|- ( ( ph /\ b e. D ) -> ( 0g ` T ) e. _V ) |
82 |
5
|
psrbag |
|- ( I e. W -> ( b e. D <-> ( b : I --> NN0 /\ ( `' b " NN ) e. Fin ) ) ) |
83 |
11 82
|
syl |
|- ( ph -> ( b e. D <-> ( b : I --> NN0 /\ ( `' b " NN ) e. Fin ) ) ) |
84 |
83
|
simplbda |
|- ( ( ph /\ b e. D ) -> ( `' b " NN ) e. Fin ) |
85 |
74
|
ffnd |
|- ( ( ph /\ b e. D ) -> b Fn I ) |
86 |
85
|
adantr |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> b Fn I ) |
87 |
15
|
ffnd |
|- ( ph -> G Fn I ) |
88 |
87
|
ad2antrr |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> G Fn I ) |
89 |
11
|
ad2antrr |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> I e. W ) |
90 |
|
eldifi |
|- ( y e. ( I \ ( `' b " NN ) ) -> y e. I ) |
91 |
90
|
adantl |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> y e. I ) |
92 |
|
fnfvof |
|- ( ( ( b Fn I /\ G Fn I ) /\ ( I e. W /\ y e. I ) ) -> ( ( b oF .^ G ) ` y ) = ( ( b ` y ) .^ ( G ` y ) ) ) |
93 |
86 88 89 91 92
|
syl22anc |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b oF .^ G ) ` y ) = ( ( b ` y ) .^ ( G ` y ) ) ) |
94 |
|
ffvelrn |
|- ( ( b : I --> NN0 /\ y e. I ) -> ( b ` y ) e. NN0 ) |
95 |
74 90 94
|
syl2an |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( b ` y ) e. NN0 ) |
96 |
|
elnn0 |
|- ( ( b ` y ) e. NN0 <-> ( ( b ` y ) e. NN \/ ( b ` y ) = 0 ) ) |
97 |
95 96
|
sylib |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b ` y ) e. NN \/ ( b ` y ) = 0 ) ) |
98 |
|
eldifn |
|- ( y e. ( I \ ( `' b " NN ) ) -> -. y e. ( `' b " NN ) ) |
99 |
98
|
adantl |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> -. y e. ( `' b " NN ) ) |
100 |
85
|
ad2antrr |
|- ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> b Fn I ) |
101 |
90
|
ad2antlr |
|- ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> y e. I ) |
102 |
|
simpr |
|- ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> ( b ` y ) e. NN ) |
103 |
100 101 102
|
elpreimad |
|- ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> y e. ( `' b " NN ) ) |
104 |
99 103
|
mtand |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> -. ( b ` y ) e. NN ) |
105 |
97 104
|
orcnd |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( b ` y ) = 0 ) |
106 |
105
|
oveq1d |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b ` y ) .^ ( G ` y ) ) = ( 0 .^ ( G ` y ) ) ) |
107 |
|
ffvelrn |
|- ( ( G : I --> C /\ y e. I ) -> ( G ` y ) e. C ) |
108 |
75 90 107
|
syl2an |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( G ` y ) e. C ) |
109 |
60 61 7
|
mulg0 |
|- ( ( G ` y ) e. C -> ( 0 .^ ( G ` y ) ) = ( 0g ` T ) ) |
110 |
108 109
|
syl |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( 0 .^ ( G ` y ) ) = ( 0g ` T ) ) |
111 |
93 106 110
|
3eqtrd |
|- ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b oF .^ G ) ` y ) = ( 0g ` T ) ) |
112 |
77 111
|
suppss |
|- ( ( ph /\ b e. D ) -> ( ( b oF .^ G ) supp ( 0g ` T ) ) C_ ( `' b " NN ) ) |
113 |
|
suppssfifsupp |
|- ( ( ( ( b oF .^ G ) e. _V /\ Fun ( b oF .^ G ) /\ ( 0g ` T ) e. _V ) /\ ( ( `' b " NN ) e. Fin /\ ( ( b oF .^ G ) supp ( 0g ` T ) ) C_ ( `' b " NN ) ) ) -> ( b oF .^ G ) finSupp ( 0g ` T ) ) |
114 |
79 80 81 84 112 113
|
syl32anc |
|- ( ( ph /\ b e. D ) -> ( b oF .^ G ) finSupp ( 0g ` T ) ) |
115 |
60 61 64 65 77 114
|
gsumcl |
|- ( ( ph /\ b e. D ) -> ( T gsum ( b oF .^ G ) ) e. C ) |
116 |
3 8
|
ringcl |
|- ( ( S e. Ring /\ ( F ` if ( b = A , H , .0. ) ) e. C /\ ( T gsum ( b oF .^ G ) ) e. C ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. C ) |
117 |
52 59 115 116
|
syl3anc |
|- ( ( ph /\ b e. D ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. C ) |
118 |
117
|
fmpttd |
|- ( ph -> ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C ) |
119 |
|
eldifsnneq |
|- ( b e. ( D \ { A } ) -> -. b = A ) |
120 |
119
|
iffalsed |
|- ( b e. ( D \ { A } ) -> if ( b = A , H , .0. ) = .0. ) |
121 |
120
|
adantl |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> if ( b = A , H , .0. ) = .0. ) |
122 |
121
|
fveq2d |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( F ` if ( b = A , H , .0. ) ) = ( F ` .0. ) ) |
123 |
|
rhmghm |
|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) ) |
124 |
14 123
|
syl |
|- ( ph -> F e. ( R GrpHom S ) ) |
125 |
16 44
|
ghmid |
|- ( F e. ( R GrpHom S ) -> ( F ` .0. ) = ( 0g ` S ) ) |
126 |
124 125
|
syl |
|- ( ph -> ( F ` .0. ) = ( 0g ` S ) ) |
127 |
126
|
adantr |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( F ` .0. ) = ( 0g ` S ) ) |
128 |
122 127
|
eqtrd |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( F ` if ( b = A , H , .0. ) ) = ( 0g ` S ) ) |
129 |
128
|
oveq1d |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( 0g ` S ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
130 |
46
|
adantr |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> S e. Ring ) |
131 |
|
eldifi |
|- ( b e. ( D \ { A } ) -> b e. D ) |
132 |
131 115
|
sylan2 |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( T gsum ( b oF .^ G ) ) e. C ) |
133 |
3 8 44
|
ringlz |
|- ( ( S e. Ring /\ ( T gsum ( b oF .^ G ) ) e. C ) -> ( ( 0g ` S ) .x. ( T gsum ( b oF .^ G ) ) ) = ( 0g ` S ) ) |
134 |
130 132 133
|
syl2anc |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( ( 0g ` S ) .x. ( T gsum ( b oF .^ G ) ) ) = ( 0g ` S ) ) |
135 |
129 134
|
eqtrd |
|- ( ( ph /\ b e. ( D \ { A } ) ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( 0g ` S ) ) |
136 |
135 51
|
suppss2 |
|- ( ph -> ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) supp ( 0g ` S ) ) C_ { A } ) |
137 |
3 44 48 51 17 118 136
|
gsumpt |
|- ( ph -> ( S gsum ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) ) |
138 |
43 137
|
eqtrd |
|- ( ph -> ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) ) |
139 |
|
iftrue |
|- ( b = A -> if ( b = A , H , .0. ) = H ) |
140 |
139
|
fveq2d |
|- ( b = A -> ( F ` if ( b = A , H , .0. ) ) = ( F ` H ) ) |
141 |
|
oveq1 |
|- ( b = A -> ( b oF .^ G ) = ( A oF .^ G ) ) |
142 |
141
|
oveq2d |
|- ( b = A -> ( T gsum ( b oF .^ G ) ) = ( T gsum ( A oF .^ G ) ) ) |
143 |
140 142
|
oveq12d |
|- ( b = A -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) ) |
144 |
|
eqid |
|- ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
145 |
|
ovex |
|- ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) e. _V |
146 |
143 144 145
|
fvmpt |
|- ( A e. D -> ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) ) |
147 |
17 146
|
syl |
|- ( ph -> ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) ) |
148 |
29 138 147
|
3eqtrd |
|- ( ph -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) ) |