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	3	ovexi	\|- U e. _V
23	22	a1i	\|- ( ph -> U e. _V )
24	2 4 21 12 23	mplelsfi	\|- ( ph -> F finSupp ( 0g ` U ) )
25		eqid	\|- ( Base ` U ) = ( Base ` U )
26	2 25 4 1 12	mplelf	\|- ( ph -> F : D --> ( Base ` U ) )
27		ssidd	\|- ( ph -> ( F supp ( 0g ` U ) ) C_ ( F supp ( 0g ` U ) ) )
28		fvexd	\|- ( ph -> ( 0g ` U ) e. _V )
29	26 27 12 28	suppssrg	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` U ) )
30		eqid	\|- ( 0g ` S ) = ( 0g ` S )
31	3 30	subrg0	\|- ( R e. ( SubRing ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
32	11 31	syl	\|- ( ph -> ( 0g ` S ) = ( 0g ` U ) )
33	32	eqcomd	\|- ( ph -> ( 0g ` U ) = ( 0g ` S ) )
34	33	adantr	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( 0g ` U ) = ( 0g ` S ) )
35	29 34	eqtrd	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( F ` b ) = ( 0g ` S ) )
36	35	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 ) ) ) ) ) )
37	10	crngringd	\|- ( ph -> S e. Ring )
38	37	adantr	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> S e. Ring )
39		eldifi	\|- ( b e. ( D \ ( F supp ( 0g ` U ) ) ) -> b e. D )
40	9	adantr	\|- ( ( ph /\ b e. D ) -> I e. V )
41	10	adantr	\|- ( ( ph /\ b e. D ) -> S e. CRing )
42	13	adantr	\|- ( ( ph /\ b e. D ) -> A e. ( K ^m I ) )
43		simpr	\|- ( ( ph /\ b e. D ) -> b e. D )
44	1 5 6 7 40 41 42 43	evlsvvvallem	\|- ( ( ph /\ b e. D ) -> ( M gsum ( v e. I \|-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K )
45	39 44	sylan2	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( M gsum ( v e. I \|-> ( ( b ` v ) .^ ( A ` v ) ) ) ) e. K )
46	5 8 30 38 45	ringlzd	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( 0g ` S ) .x. ( M gsum ( v e. I \|-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
47	36 46	eqtrd	\|- ( ( ph /\ b e. ( D \ ( F supp ( 0g ` U ) ) ) ) -> ( ( F ` b ) .x. ( M gsum ( v e. I \|-> ( ( b ` v ) .^ ( A ` v ) ) ) ) ) = ( 0g ` S ) )
48	15	a1i	\|- ( ph -> D e. _V )
49	47 48	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 ) ) )
50	17 18 20 24 49	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