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 e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlslem1.t 
|- T = ( mulGrp ` S )
evlslem1.x 
|- .^ = ( .g ` T )
evlslem1.m 
|- .x. = ( .r ` S )
evlslem1.v 
|- V = ( I mVar R )
evlslem1.e 
|- E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
evlslem1.i 
|- ( ph -> I e. W )
evlslem1.r 
|- ( ph -> R e. CRing )
evlslem1.s 
|- ( ph -> S e. CRing )
evlslem1.f 
|- ( ph -> F e. ( R RingHom S ) )
evlslem1.g 
|- ( ph -> G : I --> C )
evlslem6.y 
|- ( ph -> Y e. B )
Assertion evlslem6 
|- ( ph -> ( ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )

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 e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
5 evlslem1.t 
 |-  T = ( mulGrp ` S )
6 evlslem1.x 
 |-  .^ = ( .g ` T )
7 evlslem1.m 
 |-  .x. = ( .r ` S )
8 evlslem1.v 
 |-  V = ( I mVar R )
9 evlslem1.e 
 |-  E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
10 evlslem1.i 
 |-  ( ph -> I e. W )
11 evlslem1.r 
 |-  ( ph -> R e. CRing )
12 evlslem1.s 
 |-  ( ph -> S e. CRing )
13 evlslem1.f 
 |-  ( ph -> F e. ( R RingHom S ) )
14 evlslem1.g 
 |-  ( ph -> G : I --> C )
15 evlslem6.y 
 |-  ( ph -> Y e. B )
16 crngring 
 |-  ( S e. CRing -> S e. Ring )
17 12 16 syl 
 |-  ( ph -> S e. Ring )
18 17 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. Ring )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 19 3 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> C )
21 13 20 syl 
 |-  ( ph -> F : ( Base ` R ) --> C )
22 21 adantr 
 |-  ( ( ph /\ b e. D ) -> F : ( Base ` R ) --> C )
23 1 19 2 4 15 mplelf 
 |-  ( ph -> Y : D --> ( Base ` R ) )
24 23 ffvelcdmda 
 |-  ( ( ph /\ b e. D ) -> ( Y ` b ) e. ( Base ` R ) )
25 22 24 ffvelcdmd 
 |-  ( ( ph /\ b e. D ) -> ( F ` ( Y ` b ) ) e. C )
26 5 3 mgpbas 
 |-  C = ( Base ` T )
27 5 crngmgp 
 |-  ( S e. CRing -> T e. CMnd )
28 12 27 syl 
 |-  ( ph -> T e. CMnd )
29 28 adantr 
 |-  ( ( ph /\ b e. D ) -> T e. CMnd )
30 simpr 
 |-  ( ( ph /\ b e. D ) -> b e. D )
31 14 adantr 
 |-  ( ( ph /\ b e. D ) -> G : I --> C )
32 4 26 6 29 30 31 psrbagev2 
 |-  ( ( ph /\ b e. D ) -> ( T gsum ( b oF .^ G ) ) e. C )
33 3 7 ringcl 
 |-  ( ( S e. Ring /\ ( F ` ( Y ` b ) ) e. C /\ ( T gsum ( b oF .^ G ) ) e. C ) -> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. C )
34 18 25 32 33 syl3anc 
 |-  ( ( ph /\ b e. D ) -> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. C )
35 34 fmpttd 
 |-  ( ph -> ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C )
36 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
37 4 36 rabexd 
 |-  ( ph -> D e. _V )
38 37 mptexd 
 |-  ( ph -> ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) e. _V )
39 funmpt 
 |-  Fun ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
40 39 a1i 
 |-  ( ph -> Fun ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
41 fvexd 
 |-  ( ph -> ( 0g ` S ) e. _V )
42 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
43 1 2 42 15 mplelsfi 
 |-  ( ph -> Y finSupp ( 0g ` R ) )
44 43 fsuppimpd 
 |-  ( ph -> ( Y supp ( 0g ` R ) ) e. Fin )
45 23 feqmptd 
 |-  ( ph -> Y = ( b e. D |-> ( Y ` b ) ) )
46 45 oveq1d 
 |-  ( ph -> ( Y supp ( 0g ` R ) ) = ( ( b e. D |-> ( Y ` b ) ) supp ( 0g ` R ) ) )
47 eqimss2 
 |-  ( ( Y supp ( 0g ` R ) ) = ( ( b e. D |-> ( Y ` b ) ) supp ( 0g ` R ) ) -> ( ( b e. D |-> ( Y ` b ) ) supp ( 0g ` R ) ) C_ ( Y supp ( 0g ` R ) ) )
48 46 47 syl 
 |-  ( ph -> ( ( b e. D |-> ( Y ` b ) ) supp ( 0g ` R ) ) C_ ( Y supp ( 0g ` R ) ) )
49 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
50 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
51 42 50 ghmid 
 |-  ( F e. ( R GrpHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
52 13 49 51 3syl 
 |-  ( ph -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
53 fvexd 
 |-  ( ( ph /\ b e. D ) -> ( Y ` b ) e. _V )
54 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
55 48 52 53 54 suppssfv 
 |-  ( ph -> ( ( b e. D |-> ( F ` ( Y ` b ) ) ) supp ( 0g ` S ) ) C_ ( Y supp ( 0g ` R ) ) )
56 3 7 50 ringlz 
 |-  ( ( S e. Ring /\ x e. C ) -> ( ( 0g ` S ) .x. x ) = ( 0g ` S ) )
57 17 56 sylan 
 |-  ( ( ph /\ x e. C ) -> ( ( 0g ` S ) .x. x ) = ( 0g ` S ) )
58 fvexd 
 |-  ( ( ph /\ b e. D ) -> ( F ` ( Y ` b ) ) e. _V )
59 55 57 58 32 41 suppssov1 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) supp ( 0g ` S ) ) C_ ( Y supp ( 0g ` R ) ) )
60 suppssfifsupp 
 |-  ( ( ( ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) e. _V /\ Fun ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) /\ ( 0g ` S ) e. _V ) /\ ( ( Y supp ( 0g ` R ) ) e. Fin /\ ( ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) supp ( 0g ` S ) ) C_ ( Y supp ( 0g ` R ) ) ) ) -> ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
61 38 40 41 44 59 60 syl32anc 
 |-  ( ph -> ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
62 35 61 jca 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( Y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )