Description: Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019) (Proof shortened by AV, 31-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subrgply1.s | |
|
subrgply1.h | |
||
subrgply1.u | |
||
subrgply1.b | |
||
gsumply1subr.s | |
||
gsumply1subr.a | |
||
gsumply1subr.f | |
||
Assertion | gsumply1subr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgply1.s | |
|
2 | subrgply1.h | |
|
3 | subrgply1.u | |
|
4 | subrgply1.b | |
|
5 | gsumply1subr.s | |
|
6 | gsumply1subr.a | |
|
7 | gsumply1subr.f | |
|
8 | 1 2 3 4 | subrgply1 | |
9 | subrgsubg | |
|
10 | subgsubm | |
|
11 | 9 10 | syl | |
12 | 5 8 11 | 3syl | |
13 | eqid | |
|
14 | 6 12 7 13 | gsumsubm | |
15 | 7 6 | fexd | |
16 | ovexd | |
|
17 | 3 | fvexi | |
18 | 17 | a1i | |
19 | eqid | |
|
20 | 4 | oveq2i | |
21 | 1 2 3 19 5 20 | ressply1bas | |
22 | 21 | eqcomd | |
23 | 13 | subrgring | |
24 | 8 23 | syl | |
25 | ringmgm | |
|
26 | 5 24 25 | 3syl | |
27 | simpl | |
|
28 | 1 2 3 4 5 13 | ressply1bas | |
29 | 28 | eqcomd | |
30 | 29 | eleq2d | |
31 | 30 | biimpcd | |
32 | 31 | adantr | |
33 | 32 | impcom | |
34 | 29 | eleq2d | |
35 | 34 | biimpcd | |
36 | 35 | adantl | |
37 | 36 | impcom | |
38 | 1 2 3 4 5 13 | ressply1add | |
39 | 27 33 37 38 | syl12anc | |
40 | 39 | eqcomd | |
41 | 7 | ffund | |
42 | 7 | frnd | |
43 | 42 28 | sseqtrd | |
44 | 15 16 18 22 26 40 41 43 | gsummgmpropd | |
45 | 14 44 | eqtrd | |