Metamath Proof Explorer


Theorem gsumply1subr

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 S=Poly1R
subrgply1.h H=R𝑠T
subrgply1.u U=Poly1H
subrgply1.b B=BaseU
gsumply1subr.s φTSubRingR
gsumply1subr.a φAV
gsumply1subr.f φF:AB
Assertion gsumply1subr φSF=UF

Proof

Step Hyp Ref Expression
1 subrgply1.s S=Poly1R
2 subrgply1.h H=R𝑠T
3 subrgply1.u U=Poly1H
4 subrgply1.b B=BaseU
5 gsumply1subr.s φTSubRingR
6 gsumply1subr.a φAV
7 gsumply1subr.f φF:AB
8 1 2 3 4 subrgply1 TSubRingRBSubRingS
9 subrgsubg BSubRingSBSubGrpS
10 subgsubm BSubGrpSBSubMndS
11 9 10 syl BSubRingSBSubMndS
12 5 8 11 3syl φBSubMndS
13 eqid S𝑠B=S𝑠B
14 6 12 7 13 gsumsubm φSF=S𝑠BF
15 7 6 fexd φFV
16 ovexd φS𝑠BV
17 3 fvexi UV
18 17 a1i φUV
19 eqid BaseU=BaseU
20 4 oveq2i S𝑠B=S𝑠BaseU
21 1 2 3 19 5 20 ressply1bas φBaseU=BaseS𝑠B
22 21 eqcomd φBaseS𝑠B=BaseU
23 13 subrgring BSubRingSS𝑠BRing
24 8 23 syl TSubRingRS𝑠BRing
25 ringmgm S𝑠BRingS𝑠BMgm
26 5 24 25 3syl φS𝑠BMgm
27 simpl φsBaseS𝑠BtBaseS𝑠Bφ
28 1 2 3 4 5 13 ressply1bas φB=BaseS𝑠B
29 28 eqcomd φBaseS𝑠B=B
30 29 eleq2d φsBaseS𝑠BsB
31 30 biimpcd sBaseS𝑠BφsB
32 31 adantr sBaseS𝑠BtBaseS𝑠BφsB
33 32 impcom φsBaseS𝑠BtBaseS𝑠BsB
34 29 eleq2d φtBaseS𝑠BtB
35 34 biimpcd tBaseS𝑠BφtB
36 35 adantl sBaseS𝑠BtBaseS𝑠BφtB
37 36 impcom φsBaseS𝑠BtBaseS𝑠BtB
38 1 2 3 4 5 13 ressply1add φsBtBs+Ut=s+S𝑠Bt
39 27 33 37 38 syl12anc φsBaseS𝑠BtBaseS𝑠Bs+Ut=s+S𝑠Bt
40 39 eqcomd φsBaseS𝑠BtBaseS𝑠Bs+S𝑠Bt=s+Ut
41 7 ffund φFunF
42 7 frnd φranFB
43 42 28 sseqtrd φranFBaseS𝑠B
44 15 16 18 22 26 40 41 43 gsummgmpropd φS𝑠BF=UF
45 14 44 eqtrd φSF=UF