Theorem evlsvvvallem

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

	Ref	Expression
Hypotheses	evlsvvvallem.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	evlsvvvallem.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsvvvallem.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
	evlsvvvallem.w	⊢ ↑ = ( .g ‘ 𝑀 )
	evlsvvvallem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsvvvallem.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvvvallem.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
	evlsvvvallem.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion	evlsvvvallem	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		evlsvvvallem.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2		evlsvvvallem.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		evlsvvvallem.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
4		evlsvvvallem.w	⊢ ↑ = ( .g ‘ 𝑀 )
5		evlsvvvallem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		evlsvvvallem.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
7		evlsvvvallem.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
8		evlsvvvallem.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
9	3 2	mgpbas	⊢ 𝐾 = ( Base ‘ 𝑀 )
10		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
11	3 10	ringidval	⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑀 )
12	3	crngmgp	⊢ ( 𝑆 ∈ CRing → 𝑀 ∈ CMnd )
13	6 12	syl	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
14	6	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
15	3	ringmgp	⊢ ( 𝑆 ∈ Ring → 𝑀 ∈ Mnd )
16	14 15	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → 𝑀 ∈ Mnd )
18	1	psrbagf	⊢ ( 𝐵 ∈ 𝐷 → 𝐵 : 𝐼 ⟶ ℕ0 )
19	8 18	syl	⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ℕ0 )
20	19	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 )
21		elmapi	⊢ ( 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐾 )
22	7 21	syl	⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐾 )
23	22	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
24	9 4 17 20 23	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ∈ 𝐾 )
25	24	fmpttd	⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) : 𝐼 ⟶ 𝐾 )
26	5	mptexd	⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ∈ V )
27		fvexd	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ V )
28	25	ffund	⊢ ( 𝜑 → Fun ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
29	1	psrbagfsupp	⊢ ( 𝐵 ∈ 𝐷 → 𝐵 finSupp 0 )
30	8 29	syl	⊢ ( 𝜑 → 𝐵 finSupp 0 )
31		ssidd	⊢ ( 𝜑 → ( 𝐵 supp 0 ) ⊆ ( 𝐵 supp 0 ) )
32		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
33	19 31 5 32	suppssr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝐵 ‘ 𝑣 ) = 0 )
34	33	oveq1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 0 ↑ ( 𝐴 ‘ 𝑣 ) ) )
35		eldifi	⊢ ( 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) → 𝑣 ∈ 𝐼 )
36	35 23	sylan2	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
37	9 11 4	mulg0	⊢ ( ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 → ( 0 ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
38	36 37	syl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 0 ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
39	34 38	eqtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
40	39 5	suppss2	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) supp ( 1r ‘ 𝑆 ) ) ⊆ ( 𝐵 supp 0 ) )
41	26 27 28 30 40	fsuppsssuppgd	⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 1r ‘ 𝑆 ) )
42	9 11 13 5 25 41	gsumcl	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )