evlsvvvallem

Description: Lemma for evlsvvval akin to psrbagev2 . (Contributed by SN, 6-Mar-2025)

	Ref	Expression
Hypotheses	evlsvvvallem.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
	evlsvvvallem.k	\|- K = ( Base ` S )
	evlsvvvallem.m	\|- M = ( mulGrp ` S )
	evlsvvvallem.w	\|- .^ = ( .g ` M )
	evlsvvvallem.i	\|- ( ph -> I e. V )
	evlsvvvallem.s	\|- ( ph -> S e. CRing )
	evlsvvvallem.a	\|- ( ph -> A e. ( K ^m I ) )
	evlsvvvallem.b	\|- ( ph -> B e. D )
Assertion	evlsvvvallem	\|- ( ph -> ( M gsum ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) ) e. K )

Proof

Step	Hyp	Ref	Expression
1		evlsvvvallem.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
2		evlsvvvallem.k	\|- K = ( Base ` S )
3		evlsvvvallem.m	\|- M = ( mulGrp ` S )
4		evlsvvvallem.w	\|- .^ = ( .g ` M )
5		evlsvvvallem.i	\|- ( ph -> I e. V )
6		evlsvvvallem.s	\|- ( ph -> S e. CRing )
7		evlsvvvallem.a	\|- ( ph -> A e. ( K ^m I ) )
8		evlsvvvallem.b	\|- ( ph -> B e. D )
9	3 2	mgpbas	\|- K = ( Base ` M )
10		eqid	\|- ( 1r ` S ) = ( 1r ` S )
11	3 10	ringidval	\|- ( 1r ` S ) = ( 0g ` M )
12	3	crngmgp	\|- ( S e. CRing -> M e. CMnd )
13	6 12	syl	\|- ( ph -> M e. CMnd )
14	6	crngringd	\|- ( ph -> S e. Ring )
15	3	ringmgp	\|- ( S e. Ring -> M e. Mnd )
16	14 15	syl	\|- ( ph -> M e. Mnd )
17	16	adantr	\|- ( ( ph /\ v e. I ) -> M e. Mnd )
18	1	psrbagf	\|- ( B e. D -> B : I --> NN0 )
19	8 18	syl	\|- ( ph -> B : I --> NN0 )
20	19	ffvelcdmda	\|- ( ( ph /\ v e. I ) -> ( B ` v ) e. NN0 )
21		elmapi	\|- ( A e. ( K ^m I ) -> A : I --> K )
22	7 21	syl	\|- ( ph -> A : I --> K )
23	22	ffvelcdmda	\|- ( ( ph /\ v e. I ) -> ( A ` v ) e. K )
24	9 4 17 20 23	mulgnn0cld	\|- ( ( ph /\ v e. I ) -> ( ( B ` v ) .^ ( A ` v ) ) e. K )
25	24	fmpttd	\|- ( ph -> ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) : I --> K )
26	5	mptexd	\|- ( ph -> ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) e. _V )
27		fvexd	\|- ( ph -> ( 1r ` S ) e. _V )
28	25	ffund	\|- ( ph -> Fun ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) )
29	1	psrbagfsupp	\|- ( B e. D -> B finSupp 0 )
30	8 29	syl	\|- ( ph -> B finSupp 0 )
31		ssidd	\|- ( ph -> ( B supp 0 ) C_ ( B supp 0 ) )
32		0zd	\|- ( ph -> 0 e. ZZ )
33	19 31 5 32	suppssr	\|- ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( B ` v ) = 0 )
34	33	oveq1d	\|- ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( ( B ` v ) .^ ( A ` v ) ) = ( 0 .^ ( A ` v ) ) )
35		eldifi	\|- ( v e. ( I \ ( B supp 0 ) ) -> v e. I )
36	35 23	sylan2	\|- ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( A ` v ) e. K )
37	9 11 4	mulg0	\|- ( ( A ` v ) e. K -> ( 0 .^ ( A ` v ) ) = ( 1r ` S ) )
38	36 37	syl	\|- ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( 0 .^ ( A ` v ) ) = ( 1r ` S ) )
39	34 38	eqtrd	\|- ( ( ph /\ v e. ( I \ ( B supp 0 ) ) ) -> ( ( B ` v ) .^ ( A ` v ) ) = ( 1r ` S ) )
40	39 5	suppss2	\|- ( ph -> ( ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) supp ( 1r ` S ) ) C_ ( B supp 0 ) )
41	26 27 28 30 40	fsuppsssuppgd	\|- ( ph -> ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) finSupp ( 1r ` S ) )
42	9 11 13 5 25 41	gsumcl	\|- ( ph -> ( M gsum ( v e. I \|-> ( ( B ` v ) .^ ( A ` v ) ) ) ) e. K )

Metamath Proof Explorer

Theorem evlsvvvallem

Proof