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 ) )

Metamath Proof Explorer

Theorem evlsvvvallem2

Proof