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 = Poly 1 R
subrgply1.h H = R 𝑠 T
subrgply1.u U = Poly 1 H
subrgply1.b B = Base U
gsumply1subr.s φ T SubRing R
gsumply1subr.a φ A V
gsumply1subr.f φ F : A B
Assertion gsumply1subr φ S F = U F

Proof

Step Hyp Ref Expression
1 subrgply1.s S = Poly 1 R
2 subrgply1.h H = R 𝑠 T
3 subrgply1.u U = Poly 1 H
4 subrgply1.b B = Base U
5 gsumply1subr.s φ T SubRing R
6 gsumply1subr.a φ A V
7 gsumply1subr.f φ F : A B
8 1 2 3 4 subrgply1 T SubRing R B SubRing S
9 subrgsubg B SubRing S B SubGrp S
10 subgsubm B SubGrp S B SubMnd S
11 5 8 9 10 4syl φ B SubMnd S
12 eqid S 𝑠 B = S 𝑠 B
13 6 11 7 12 gsumsubm φ S F = S 𝑠 B F
14 7 6 fexd φ F V
15 ovexd φ S 𝑠 B V
16 3 fvexi U V
17 16 a1i φ U V
18 eqid Base U = Base U
19 4 oveq2i S 𝑠 B = S 𝑠 Base U
20 1 2 3 18 5 19 ressply1bas φ Base U = Base S 𝑠 B
21 20 eqcomd φ Base S 𝑠 B = Base U
22 12 subrgring B SubRing S S 𝑠 B Ring
23 ringmgm S 𝑠 B Ring S 𝑠 B Mgm
24 5 8 22 23 4syl φ S 𝑠 B Mgm
25 simpl φ s Base S 𝑠 B t Base S 𝑠 B φ
26 1 2 3 4 5 12 ressply1bas φ B = Base S 𝑠 B
27 26 eqcomd φ Base S 𝑠 B = B
28 27 eleq2d φ s Base S 𝑠 B s B
29 28 biimpcd s Base S 𝑠 B φ s B
30 29 adantr s Base S 𝑠 B t Base S 𝑠 B φ s B
31 30 impcom φ s Base S 𝑠 B t Base S 𝑠 B s B
32 27 eleq2d φ t Base S 𝑠 B t B
33 32 biimpcd t Base S 𝑠 B φ t B
34 33 adantl s Base S 𝑠 B t Base S 𝑠 B φ t B
35 34 impcom φ s Base S 𝑠 B t Base S 𝑠 B t B
36 1 2 3 4 5 12 ressply1add φ s B t B s + U t = s + S 𝑠 B t
37 25 31 35 36 syl12anc φ s Base S 𝑠 B t Base S 𝑠 B s + U t = s + S 𝑠 B t
38 37 eqcomd φ s Base S 𝑠 B t Base S 𝑠 B s + S 𝑠 B t = s + U t
39 7 ffund φ Fun F
40 7 frnd φ ran F B
41 40 26 sseqtrd φ ran F Base S 𝑠 B
42 14 15 17 21 24 38 39 41 gsummgmpropd φ S 𝑠 B F = U F
43 13 42 eqtrd φ S F = U F