Metamath Proof Explorer

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 ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )