Metamath Proof Explorer


Theorem evlslem6

Description: Lemma for evlseu . Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 26-Jul-2019) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem1.p P = I mPoly R
evlslem1.b B = Base P
evlslem1.c C = Base S
evlslem1.d D = h 0 I | h -1 Fin
evlslem1.t T = mulGrp S
evlslem1.x × ˙ = T
evlslem1.m · ˙ = S
evlslem1.v V = I mVar R
evlslem1.e E = p B S b D F p b · ˙ T b × ˙ f G
evlslem1.i φ I W
evlslem1.r φ R CRing
evlslem1.s φ S CRing
evlslem1.f φ F R RingHom S
evlslem1.g φ G : I C
evlslem6.y φ Y B
Assertion evlslem6 φ b D F Y b · ˙ T b × ˙ f G : D C finSupp 0 S b D F Y b · ˙ T b × ˙ f G

Proof

Step Hyp Ref Expression
1 evlslem1.p P = I mPoly R
2 evlslem1.b B = Base P
3 evlslem1.c C = Base S
4 evlslem1.d D = h 0 I | h -1 Fin
5 evlslem1.t T = mulGrp S
6 evlslem1.x × ˙ = T
7 evlslem1.m · ˙ = S
8 evlslem1.v V = I mVar R
9 evlslem1.e E = p B S b D F p b · ˙ T b × ˙ f G
10 evlslem1.i φ I W
11 evlslem1.r φ R CRing
12 evlslem1.s φ S CRing
13 evlslem1.f φ F R RingHom S
14 evlslem1.g φ G : I C
15 evlslem6.y φ Y B
16 crngring S CRing S Ring
17 12 16 syl φ S Ring
18 17 adantr φ b D S Ring
19 eqid Base R = Base R
20 19 3 rhmf F R RingHom S F : Base R C
21 13 20 syl φ F : Base R C
22 21 adantr φ b D F : Base R C
23 1 19 2 4 15 mplelf φ Y : D Base R
24 23 ffvelrnda φ b D Y b Base R
25 22 24 ffvelrnd φ b D F Y b C
26 5 3 mgpbas C = Base T
27 5 crngmgp S CRing T CMnd
28 12 27 syl φ T CMnd
29 28 adantr φ b D T CMnd
30 simpr φ b D b D
31 14 adantr φ b D G : I C
32 4 26 6 29 30 31 psrbagev2 φ b D T b × ˙ f G C
33 3 7 ringcl S Ring F Y b C T b × ˙ f G C F Y b · ˙ T b × ˙ f G C
34 18 25 32 33 syl3anc φ b D F Y b · ˙ T b × ˙ f G C
35 34 fmpttd φ b D F Y b · ˙ T b × ˙ f G : D C
36 ovexd φ 0 I V
37 4 36 rabexd φ D V
38 37 mptexd φ b D F Y b · ˙ T b × ˙ f G V
39 funmpt Fun b D F Y b · ˙ T b × ˙ f G
40 39 a1i φ Fun b D F Y b · ˙ T b × ˙ f G
41 fvexd φ 0 S V
42 eqid 0 R = 0 R
43 1 2 42 15 11 mplelsfi φ finSupp 0 R Y
44 43 fsuppimpd φ Y supp 0 R Fin
45 23 feqmptd φ Y = b D Y b
46 45 oveq1d φ Y supp 0 R = b D Y b supp 0 R
47 eqimss2 Y supp 0 R = b D Y b supp 0 R b D Y b supp 0 R Y supp 0 R
48 46 47 syl φ b D Y b supp 0 R Y supp 0 R
49 rhmghm F R RingHom S F R GrpHom S
50 eqid 0 S = 0 S
51 42 50 ghmid F R GrpHom S F 0 R = 0 S
52 13 49 51 3syl φ F 0 R = 0 S
53 fvexd φ b D Y b V
54 fvexd φ 0 R V
55 48 52 53 54 suppssfv φ b D F Y b supp 0 S Y supp 0 R
56 3 7 50 ringlz S Ring x C 0 S · ˙ x = 0 S
57 17 56 sylan φ x C 0 S · ˙ x = 0 S
58 fvexd φ b D F Y b V
59 55 57 58 32 41 suppssov1 φ b D F Y b · ˙ T b × ˙ f G supp 0 S Y supp 0 R
60 suppssfifsupp b D F Y b · ˙ T b × ˙ f G V Fun b D F Y b · ˙ T b × ˙ f G 0 S V Y supp 0 R Fin b D F Y b · ˙ T b × ˙ f G supp 0 S Y supp 0 R finSupp 0 S b D F Y b · ˙ T b × ˙ f G
61 38 40 41 44 59 60 syl32anc φ finSupp 0 S b D F Y b · ˙ T b × ˙ f G
62 35 61 jca φ b D F Y b · ˙ T b × ˙ f G : D C finSupp 0 S b D F Y b · ˙ T b × ˙ f G