This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evlsvvvallem2

Description: Lemma for theorems using evlsvvval . (Contributed by SN, 8-Mar-2025)

Ref Expression
Hypotheses evlsvvvallem2.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlsvvvallem2.p 
|- P = ( I mPoly U )
evlsvvvallem2.u 
|- U = ( S |`s R )
evlsvvvallem2.b 
|- B = ( Base ` P )
evlsvvvallem2.k 
|- K = ( Base ` S )
evlsvvvallem2.m 
|- M = ( mulGrp ` S )
evlsvvvallem2.w 
|- .^ = ( .g ` M )
evlsvvvallem2.x 
|- .x. = ( .r ` S )
evlsvvvallem2.i 
|- ( ph -> I e. V )
evlsvvvallem2.s 
|- ( ph -> S e. CRing )
evlsvvvallem2.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsvvvallem2.f 
|- ( ph -> F e. B )
evlsvvvallem2.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion evlsvvvallem2 
|- ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` S ) )

Proof

Step Hyp Ref Expression
1 evlsvvvallem2.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2 evlsvvvallem2.p 
 |-  P = ( I mPoly U )
3 evlsvvvallem2.u 
 |-  U = ( S |`s R )
4 evlsvvvallem2.b 
 |-  B = ( Base ` P )
5 evlsvvvallem2.k 
 |-  K = ( Base ` S )
6 evlsvvvallem2.m 
 |-  M = ( mulGrp ` S )
7 evlsvvvallem2.w 
 |-  .^ = ( .g ` M )
8 evlsvvvallem2.x 
 |-  .x. = ( .r ` S )
9 evlsvvvallem2.i 
 |-  ( ph -> I e. V )
10 evlsvvvallem2.s 
 |-  ( ph -> S e. CRing )
11 evlsvvvallem2.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
12 evlsvvvallem2.f 
 |-  ( ph -> F e. B )
13 evlsvvvallem2.a 
 |-  ( ph -> A e. ( K ^m I ) )
14 ovex 
 |-  ( NN0 ^m I ) e. _V
15 1 14 rabex2 
 |-  D e. _V
16 15 mptex 
 |-  ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) e. _V
17 16 a1i 
 |-  ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) e. _V )
18 fvexd 
 |-  ( ph -> ( 0g ` S ) e. _V )
19 funmpt 
 |-  Fun ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) )
20 19 a1i 
 |-  ( ph -> Fun ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) )
21 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
22 2 4 21 12 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` U ) )
23 eqid 
 |-  ( Base ` U ) = ( Base ` U )
24 2 23 4 1 12 mplelf 
 |-  ( ph -> F : D --> ( Base ` U ) )
25 ssidd 
 |-  ( ph -> ( F supp ( 0g ` U ) ) C_ ( F supp ( 0g ` U ) ) )
26 fvexd 
 |-  ( ph -> ( 0g ` U ) e. _V )
27 24 25 12 26 suppssrg 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` U ) )
28 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
29 3 28 subrg0 
 |-  ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
30 11 29 syl 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
31 30 eqcomd 
 |-  ( ph -> ( 0g ` U ) = ( 0g ` S ) )
32 31 adantr 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( 0g ` U ) = ( 0g ` S ) )
33 27 32 eqtrd 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` S ) )
34 33 oveq1d 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( ( 0g ` S ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) )
35 10 crngringd 
 |-  ( ph -> S e. Ring )
36 35 adantr 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> S e. Ring )
37 eldifi 
 |-  ( b e. ( D \ ( F supp ( 0g ` U ) ) ) -> b e. D )
38 9 adantr 
 |-  ( ( ph /\ b e. D ) -> I e. V )
39 10 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. CRing )
40 13 adantr 
 |-  ( ( ph /\ b e. D ) -> A e. ( K ^m I ) )
41 simpr 
 |-  ( ( ph /\ b e. D ) -> b e. D )
42 1 5 6 7 38 39 40 41 evlsvvvallem 
 |-  ( ( ph /\ b e. D ) -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K )
43 37 42 sylan2 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K )
44 5 8 28 36 43 ringlzd 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( 0g ` S ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
45 34 44 eqtrd 
 |-  ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
46 15 a1i 
 |-  ( ph -> D e. _V )
47 45 46 suppss2 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) supp ( 0g ` S ) ) C_ ( F supp ( 0g ` U ) ) )
48 17 18 20 22 47 fsuppsssuppgd 
 |-  ( ph -> ( b e. D |-> ( ( F ` b ) .x. ( M gsum ( v e. I |-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) ) finSupp ( 0g ` S ) )