Theorem evlsvvval

Description: Give a formula for the evaluation of a polynomial given assignments from variables to values. This is the sum of the evaluations for each term (corresponding to a bag of variables), that is, the coefficient times the product of each variable raised to the corresponding power. (Contributed by SN, 5-Mar-2025)

	Ref	Expression
Hypotheses	evlsvvval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsvvval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
	evlsvvval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlsvvval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsvvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	evlsvvval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsvvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
	evlsvvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
	evlsvvval.x	⊢ · = ( .r ‘ 𝑆 )
	evlsvvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsvvval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvvval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsvvval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	evlsvvval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlsvvval	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvvval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsvvval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsvvval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		evlsvvval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		evlsvvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
6		evlsvvval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
7		evlsvvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
8		evlsvvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
9		evlsvvval.x	⊢ · = ( .r ‘ 𝑆 )
10		evlsvvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		evlsvvval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
12		evlsvvval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
13		evlsvvval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
14		evlsvvval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
15		fveq1	⊢ ( 𝑙 = 𝐴 → ( 𝑙 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
16	15	oveq2d	⊢ ( 𝑙 = 𝐴 → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) = ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) )
17	16	mpteq2dv	⊢ ( 𝑙 = 𝐴 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) )
18	17	oveq2d	⊢ ( 𝑙 = 𝐴 → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) = ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) )
19	18	oveq2d	⊢ ( 𝑙 = 𝐴 → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) = ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
20	19	mpteq2dv	⊢ ( 𝑙 = 𝐴 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) )
21	20	oveq2d	⊢ ( 𝑙 = 𝐴 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
22		eqid	⊢ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
23		eqid	⊢ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
24		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
25		eqid	⊢ ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
26		eqid	⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) )
27		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) )
28	1 2 3 5 6 4 22 23 24 25 26 27 10 11 12 13	evlsvval	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
29		sneq	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑏 ) → { 𝑥 } = { ( 𝐹 ‘ 𝑏 ) } )
30	29	xpeq2d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) = ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) )
31		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
32	2 31 3 5 13	mplelf	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) )
33	4	subrgbas	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
34	12 33	syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
35	34	feq3d	⊢ ( 𝜑 → ( 𝐹 : 𝐷 ⟶ 𝑅 ↔ 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) ) )
36	32 35	mpbird	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
37	36	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑅 )
38		ovex	⊢ ( 𝐾 ↑m 𝐼 ) ∈ V
39		snex	⊢ { ( 𝐹 ‘ 𝑏 ) } ∈ V
40	38 39	xpex	⊢ ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ∈ V
41	40	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ∈ V )
42	26 30 37 41	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) )
43	5	psrbagf	⊢ ( 𝑏 ∈ 𝐷 → 𝑏 : 𝐼 ⟶ ℕ0 )
44	43	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 : 𝐼 ⟶ ℕ0 )
45	44	ffnd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 Fn 𝐼 )
46	38	mptex	⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ V
47	46 27	fnmpti	⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) Fn 𝐼
48	47	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) Fn 𝐼 )
49	10	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
50		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
51		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑖 ) = ( 𝑏 ‘ 𝑖 ) )
52		fveq2	⊢ ( 𝑥 = 𝑖 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑖 ) )
53	52	mpteq2dv	⊢ ( 𝑥 = 𝑖 → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) )
54		simpr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
55		eqid	⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
56	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ CRing )
57		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
58		elmapi	⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ 𝐾 )
59	58	ffvelcdmda	⊢ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑖 ) ∈ 𝐾 )
60	59	ancoms	⊢ ( ( 𝑖 ∈ 𝐼 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑖 ) ∈ 𝐾 )
61	60	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑖 ) ∈ 𝐾 )
62	61	fmpttd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
63	22 6 55 56 57 62	pwselbasr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
64	27 53 54 63	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ‘ 𝑖 ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) )
65	45 48 49 49 50 51 64	offval	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) ) )
66	23 55	mgpbas	⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
67	11	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
68		ovexd	⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
69	22	pwsring	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring )
70	67 68 69	syl2anc	⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring )
71	23	ringmgp	⊢ ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd )
72	70 71	syl	⊢ ( 𝜑 → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd )
73	72	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd )
74	44	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑖 ) ∈ ℕ0 )
75	66 24 73 74 63	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
76	22 6 55 56 57 75	pwselbas	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
77	76	ffnd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) Fn ( 𝐾 ↑m 𝐼 ) )
78		ovex	⊢ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ∈ V
79		eqid	⊢ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) )
80	78 79	fnmpti	⊢ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) Fn ( 𝐾 ↑m 𝐼 )
81	80	a1i	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) Fn ( 𝐾 ↑m 𝐼 ) )
82		eqid	⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) )
83		fveq1	⊢ ( 𝑎 = 𝑝 → ( 𝑎 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) )
84		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) )
85		fvexd	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ V )
86	82 83 84 85	fvmptd3	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ‘ 𝑝 ) = ( 𝑝 ‘ 𝑖 ) )
87	86	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑏 ‘ 𝑖 ) ↑ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ‘ 𝑝 ) ) = ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑝 ‘ 𝑖 ) ) )
88	67	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑆 ∈ Ring )
89		ovexd	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
90	74	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℕ0 )
91	63	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
92	22 55 23 7 24 8 88 89 90 91 84	pwsexpg	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) ‘ 𝑝 ) = ( ( 𝑏 ‘ 𝑖 ) ↑ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ‘ 𝑝 ) ) )
93		fveq1	⊢ ( 𝑚 = 𝑝 → ( 𝑚 ‘ 𝑖 ) = ( 𝑝 ‘ 𝑖 ) )
94	93	oveq2d	⊢ ( 𝑚 = 𝑝 → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) = ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑝 ‘ 𝑖 ) ) )
95		ovexd	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑝 ‘ 𝑖 ) ) ∈ V )
96	79 94 84 95	fvmptd3	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ‘ 𝑝 ) = ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑝 ‘ 𝑖 ) ) )
97	87 92 96	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑝 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) ‘ 𝑝 ) = ( ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ‘ 𝑝 ) )
98	77 81 97	eqfnfvd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) )
99	98	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) )
100	65 99	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) )
101	100	oveq2d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) )
102		eqid	⊢ ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
103		ovexd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
104	11	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing )
105	7 6	mgpbas	⊢ 𝐾 = ( Base ‘ 𝑀 )
106	7	ringmgp	⊢ ( 𝑆 ∈ Ring → 𝑀 ∈ Mnd )
107	67 106	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
108	107	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ 𝐼 ) ) → 𝑀 ∈ Mnd )
109	74	adantrl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ 𝐼 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℕ0 )
110		elmapi	⊢ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) → 𝑚 : 𝐼 ⟶ 𝐾 )
111	110	ffvelcdmda	⊢ ( ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑚 ‘ 𝑖 ) ∈ 𝐾 )
112	111	adantl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ 𝐼 ) ) → ( 𝑚 ‘ 𝑖 ) ∈ 𝐾 )
113	105 8 108 109 112	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ 𝐼 ) ) → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ∈ 𝐾 )
114	49	mptexd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ∈ V )
115		fvexd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ V )
116		funmpt	⊢ Fun ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) )
117	116	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → Fun ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) )
118	5	psrbagfsupp	⊢ ( 𝑏 ∈ 𝐷 → 𝑏 finSupp 0 )
119	118	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 finSupp 0 )
120		ssidd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 supp 0 ) ⊆ ( 𝑏 supp 0 ) )
121		0cnd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 0 ∈ ℂ )
122	44 120 49 121	suppssr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑏 ‘ 𝑖 ) = 0 )
123	122	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) = ( 0 ↑ ( 𝑚 ‘ 𝑖 ) ) )
124	123	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) = ( 0 ↑ ( 𝑚 ‘ 𝑖 ) ) )
125		eldifi	⊢ ( 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) → 𝑖 ∈ 𝐼 )
126	125 111	sylan2	⊢ ( ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑚 ‘ 𝑖 ) ∈ 𝐾 )
127	126	ancoms	⊢ ( ( 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑚 ‘ 𝑖 ) ∈ 𝐾 )
128	127	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑚 ‘ 𝑖 ) ∈ 𝐾 )
129		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
130	7 129	ringidval	⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑀 )
131	105 130 8	mulg0	⊢ ( ( 𝑚 ‘ 𝑖 ) ∈ 𝐾 → ( 0 ↑ ( 𝑚 ‘ 𝑖 ) ) = ( 1r ‘ 𝑆 ) )
132	128 131	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 0 ↑ ( 𝑚 ‘ 𝑖 ) ) = ( 1r ‘ 𝑆 ) )
133	124 132	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) = ( 1r ‘ 𝑆 ) )
134	133	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 1r ‘ 𝑆 ) ) )
135		fconstmpt	⊢ ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 1r ‘ 𝑆 ) )
136	22 129	pws1	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
137	67 68 136	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
138	137	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
139	135 138	eqtr3id	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
140	134 139	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐼 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
141	140 49	suppss2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) supp ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ⊆ ( 𝑏 supp 0 ) )
142	114 115 117 119 141	fsuppsssuppgd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) finSupp ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
143	22 6 102 23 7 103 49 104 113 142	pwsgprod	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑖 ∈ 𝐼 ↦ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) )
144	101 143	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) )
145	42 144	oveq12d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) ) )
146	6	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
147	33 146	eqsstrrd	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
148	12 147	syl	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
149	32 148	fssd	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐾 )
150	149	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 )
151		fconst6g	⊢ ( ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 → ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
152	150 151	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
153	22 6 55 104 103 152	pwselbasr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
154	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝐼 ∈ 𝑉 )
155	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑆 ∈ CRing )
156		simpr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) )
157		simplr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑏 ∈ 𝐷 )
158	5 6 7 8 154 155 156 157	evlsvvvallem	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ∈ 𝐾 )
159	158	fmpttd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
160	22 6 55 104 103 159	pwselbasr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
161	22 55 104 103 153 160 9 25	pwsmulrval	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) ) = ( ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ∘f · ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) ) )
162	152	ffnd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) Fn ( 𝐾 ↑m 𝐼 ) )
163		ovex	⊢ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ∈ V
164		eqid	⊢ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) = ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) )
165	163 164	fnmpti	⊢ ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) Fn ( 𝐾 ↑m 𝐼 )
166	165	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) Fn ( 𝐾 ↑m 𝐼 ) )
167		inidm	⊢ ( ( 𝐾 ↑m 𝐼 ) ∩ ( 𝐾 ↑m 𝐼 ) ) = ( 𝐾 ↑m 𝐼 )
168		fvex	⊢ ( 𝐹 ‘ 𝑏 ) ∈ V
169	168	fvconst2	⊢ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) → ( ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ‘ 𝑙 ) = ( 𝐹 ‘ 𝑏 ) )
170	169	adantl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ‘ 𝑙 ) = ( 𝐹 ‘ 𝑏 ) )
171		fveq1	⊢ ( 𝑚 = 𝑙 → ( 𝑚 ‘ 𝑖 ) = ( 𝑙 ‘ 𝑖 ) )
172	171	oveq2d	⊢ ( 𝑚 = 𝑙 → ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) = ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) )
173	172	mpteq2dv	⊢ ( 𝑚 = 𝑙 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) )
174	173	oveq2d	⊢ ( 𝑚 = 𝑙 → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) = ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) )
175		simpr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) )
176	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝐼 ∈ 𝑉 )
177	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑆 ∈ CRing )
178		simplr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑏 ∈ 𝐷 )
179	5 6 7 8 176 177 175 178	evlsvvvallem	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ∈ 𝐾 )
180	164 174 175 179	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) ‘ 𝑙 ) = ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) )
181	162 166 103 103 167 170 180	offval	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( ( 𝐾 ↑m 𝐼 ) × { ( 𝐹 ‘ 𝑏 ) } ) ∘f · ( 𝑚 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑚 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) )
182	145 161 181	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) )
183	182	mpteq2dva	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) )
184	183	oveq2d	⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) ) )
185		eqid	⊢ ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
186		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
187	5 186	rabexd	⊢ ( 𝜑 → 𝐷 ∈ V )
188	67	ringcmnd	⊢ ( 𝜑 → 𝑆 ∈ CMnd )
189	67	adantr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑆 ∈ Ring )
190	150	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 )
191		simpl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝜑 )
192		simprr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑏 ∈ 𝐷 )
193		simprl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) )
194	191 192 193 179	syl21anc	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ∈ 𝐾 )
195	6 9 189 190 194	ringcld	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ∈ 𝐾 )
196	187	mptexd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) ∈ V )
197		fvexd	⊢ ( 𝜑 → ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ V )
198		funmpt	⊢ Fun ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) )
199	198	a1i	⊢ ( 𝜑 → Fun ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) )
200		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
201	4	ovexi	⊢ 𝑈 ∈ V
202	201	a1i	⊢ ( 𝜑 → 𝑈 ∈ V )
203	2 3 200 13 202	mplelsfi	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑈 ) )
204		ssidd	⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
205		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ V )
206	149 204 187 205	suppssr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑈 ) )
207		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
208	4 207	subrg0	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
209	12 208	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
210	209	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
211	206 210	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) )
212	211	adantr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) )
213	212	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) )
214	67	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑆 ∈ Ring )
215		eldifi	⊢ ( 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) → 𝑏 ∈ 𝐷 )
216	215 179	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ∈ 𝐾 )
217	6 9 207 214 216	ringlzd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
218	213 217	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
219	218	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 0g ‘ 𝑆 ) ) )
220		fconstmpt	⊢ ( ( 𝐾 ↑m 𝐼 ) × { ( 0g ‘ 𝑆 ) } ) = ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 0g ‘ 𝑆 ) )
221	188	cmnmndd	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
222	22 207	pws0g	⊢ ( ( 𝑆 ∈ Mnd ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
223	221 68 222	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
224	220 223	eqtr3id	⊢ ( 𝜑 → ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
225	224	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
226	219 225	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
227	226 187	suppss2	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) supp ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑈 ) ) )
228	196 197 199 203 227	fsuppsssuppgd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) finSupp ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
229	22 6 185 68 187 188 195 228	pwsgsum	⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) ) )
230	28 184 229	3eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝑙 ‘ 𝑖 ) ) ) ) ) ) ) ) )
231		ovexd	⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) ∈ V )
232	21 230 14 231	fvmptd4	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )