Metamath Proof Explorer

Theorem evlsbagval

Description: Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since .0. and .1. using U instead of S is convenient for its sole use case mhphf , but may not be convenient for other uses. (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses evlsbagval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsbagval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
evlsbagval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsbagval.w ⊢ 𝑊 = ( Base ‘ 𝑃 )
evlsbagval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlsbagval.m ⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
evlsbagval.e ⊢ ↑ = ( .g ‘ 𝑀 )
evlsbagval.z ⊢ 0 = ( 0g ‘ 𝑈 )
evlsbagval.o ⊢ 1 = ( 1r ‘ 𝑈 )
evlsbagval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
evlsbagval.f ⊢ 𝐹 = ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝐵 , 1 , 0 ) )
evlsbagval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsbagval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsbagval.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsbagval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
evlsbagval.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion evlsbagval ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 evlsbagval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsbagval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3 evlsbagval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4 evlsbagval.w ⊢ 𝑊 = ( Base ‘ 𝑃 )
5 evlsbagval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 evlsbagval.m ⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
7 evlsbagval.e ⊢ ↑ = ( .g ‘ 𝑀 )
8 evlsbagval.z ⊢ 0 = ( 0g ‘ 𝑈 )
9 evlsbagval.o ⊢ 1 = ( 1r ‘ 𝑈 )
10 evlsbagval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 evlsbagval.f ⊢ 𝐹 = ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝐵 , 1 , 0 ) )
12 evlsbagval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
13 evlsbagval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
14 evlsbagval.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
15 evlsbagval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
16 evlsbagval.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
17 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ∈ V )
18 ovexd ⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
19 10 18 rabexd ⊢ ( 𝜑 → 𝐷 ∈ V )
20 3 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
21 14 20 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
22 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
23 22 9 ringidcl ⊢ ( 𝑈 ∈ Ring → 1 ∈ ( Base ‘ 𝑈 ) )
24 21 23 syl ⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑈 ) )
25 22 8 ring0cl ⊢ ( 𝑈 ∈ Ring → 0 ∈ ( Base ‘ 𝑈 ) )
26 21 25 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑈 ) )
27 24 26 ifcld ⊢ ( 𝜑 → if ( 𝑠 = 𝐵 , 1 , 0 ) ∈ ( Base ‘ 𝑈 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → if ( 𝑠 = 𝐵 , 1 , 0 ) ∈ ( Base ‘ 𝑈 ) )
29 28 11 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) )
30 17 19 29 elmapdd ⊢ ( 𝜑 → 𝐹 ∈ ( ( Base ‘ 𝑈 ) ↑m 𝐷 ) )
31 eqid ⊢ ( 𝐼 mPwSer 𝑈 ) = ( 𝐼 mPwSer 𝑈 )
32 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑈 ) )
33 31 22 10 32 12 psrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) = ( ( Base ‘ 𝑈 ) ↑m 𝐷 ) )
34 30 33 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) )
35 19 26 11 sniffsupp ⊢ ( 𝜑 → 𝐹 finSupp 0 )
36 2 31 32 8 4 mplelbas ⊢ ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) ∧ 𝐹 finSupp 0 ) )
37 34 35 36 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
38 fveq1 ⊢ ( 𝑝 = 𝐹 → ( 𝑝 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
39 38 fveq2d ⊢ ( 𝑝 = 𝐹 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) = ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) )
40 39 oveq1d ⊢ ( 𝑝 = 𝐹 → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
41 40 mpteq2dv ⊢ ( 𝑝 = 𝐹 → ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) )
42 41 oveq2d ⊢ ( 𝑝 = 𝐹 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
43 eqid ⊢ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
44 eqid ⊢ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
45 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
46 eqid ⊢ ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
47 eqid ⊢ ( 𝑝 ∈ 𝑊 ↦ ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ) = ( 𝑝 ∈ 𝑊 ↦ ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
48 eqid ⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) )
49 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) )
50 1 2 4 10 5 3 43 44 45 46 47 48 49 12 13 14 evlsval3 ⊢ ( 𝜑 → 𝑄 = ( 𝑝 ∈ 𝑊 ↦ ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝑝 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ) )
51 ovexd ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ∈ V )
52 42 50 37 51 fvmptd4 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
53 52 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ‘ 𝐴 ) )
54 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
55 eqid ⊢ ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
56 13 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
57 ovexd ⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
58 43 pwsring ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring )
59 56 57 58 syl2anc ⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring )
60 59 ringcmnd ⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ CMnd )
61 59 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring )
62 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑅 ) → 𝑆 ∈ CRing )
63 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑅 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
64 5 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
65 14 64 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑅 ⊆ 𝐾 )
67 66 sselda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ 𝐾 )
68 fconst6g ⊢ ( 𝑥 ∈ 𝐾 → ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
69 67 68 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
70 43 5 54 62 63 69 pwselbasr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
71 70 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) : 𝑅 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
72 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
73 3 72 subrg1 ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑈 ) )
74 14 73 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑈 ) )
75 72 subrg1cl ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 1r ‘ 𝑆 ) ∈ 𝑅 )
76 14 75 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ 𝑅 )
77 74 76 eqeltrrd ⊢ ( 𝜑 → ( 1r ‘ 𝑈 ) ∈ 𝑅 )
78 9 77 eqeltrid ⊢ ( 𝜑 → 1 ∈ 𝑅 )
79 3 subrgbas ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
80 14 79 syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
81 26 80 eleqtrrd ⊢ ( 𝜑 → 0 ∈ 𝑅 )
82 78 81 ifcld ⊢ ( 𝜑 → if ( 𝑠 = 𝐵 , 1 , 0 ) ∈ 𝑅 )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → if ( 𝑠 = 𝐵 , 1 , 0 ) ∈ 𝑅 )
84 83 11 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝑅 )
85 84 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑅 )
86 71 85 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
87 44 54 mgpbas ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
88 43 pwscrng ⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ CRing )
89 13 57 88 syl2anc ⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ CRing )
90 44 crngmgp ⊢ ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ CRing → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ CMnd )
91 89 90 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ CMnd )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ CMnd )
93 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
94 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ CRing )
95 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
96 elmapi ⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ 𝐾 )
97 96 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 )
98 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑥 ∈ 𝐼 )
99 97 98 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐾 )
100 99 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
101 43 5 54 94 95 100 pwselbasr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
102 101 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
103 10 87 45 92 93 102 psrbagev2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
104 54 46 61 86 103 ringcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
105 104 fmpttd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) : 𝐷 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
106 eqeq1 ⊢ ( 𝑠 = 𝑏 → ( 𝑠 = 𝐵 ↔ 𝑏 = 𝐵 ) )
107 106 ifbid ⊢ ( 𝑠 = 𝑏 → if ( 𝑠 = 𝐵 , 1 , 0 ) = if ( 𝑏 = 𝐵 , 1 , 0 ) )
108 eldifi ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) → 𝑏 ∈ 𝐷 )
109 108 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → 𝑏 ∈ 𝐷 )
110 9 fvexi ⊢ 1 ∈ V
111 8 fvexi ⊢ 0 ∈ V
112 110 111 ifex ⊢ if ( 𝑏 = 𝐵 , 1 , 0 ) ∈ V
113 112 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → if ( 𝑏 = 𝐵 , 1 , 0 ) ∈ V )
114 11 107 109 113 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑏 ) = if ( 𝑏 = 𝐵 , 1 , 0 ) )
115 eldifsnneq ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) → ¬ 𝑏 = 𝐵 )
116 115 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ¬ 𝑏 = 𝐵 )
117 116 iffalsed ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → if ( 𝑏 = 𝐵 , 1 , 0 ) = 0 )
118 114 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑏 ) = 0 )
119 118 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 0 ) )
120 sneq ⊢ ( 𝑥 = 0 → { 𝑥 } = { 0 } )
121 120 xpeq2d ⊢ ( 𝑥 = 0 → ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) = ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) )
122 81 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → 0 ∈ 𝑅 )
123 ovex ⊢ ( 𝐾 ↑m 𝐼 ) ∈ V
124 snex ⊢ { 0 } ∈ V
125 123 124 xpex ⊢ ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) ∈ V
126 125 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) ∈ V )
127 48 121 122 126 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 0 ) = ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) )
128 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
129 3 128 subrg0 ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
130 14 129 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
131 130 8 eqtr4di ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = 0 )
132 131 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝑆 ) } = { 0 } )
133 132 xpeq2d ⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { ( 0g ‘ 𝑆 ) } ) = ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) )
134 56 ringgrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
135 134 grpmndd ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
136 43 128 pws0g ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
137 135 57 136 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
138 133 137 eqtr3d ⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝐾 ↑m 𝐼 ) × { 0 } ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
140 119 127 139 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
141 140 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
142 91 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ CMnd )
143 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ CRing )
144 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
145 96 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 )
146 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑥 ∈ 𝐼 )
147 145 146 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐾 )
148 147 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
149 43 5 54 143 144 148 pwselbasr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
150 149 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
151 10 87 45 142 109 150 psrbagev2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
152 54 46 55 ringlz ⊢ ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring ∧ ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) → ( ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
153 59 151 152 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
154 141 153 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
155 154 19 suppss2 ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) supp ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ⊆ { 𝐵 } )
156 19 mptexd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ∈ V )
157 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ V )
158 funmpt ⊢ Fun ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
159 158 a1i ⊢ ( 𝜑 → Fun ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) )
160 snfi ⊢ { 𝐵 } ∈ Fin
161 160 a1i ⊢ ( 𝜑 → { 𝐵 } ∈ Fin )
162 161 155 ssfid ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) supp ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ∈ Fin )
163 156 157 159 162 isfsuppd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) finSupp ( 0g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
164 54 55 60 19 105 155 163 gsumres ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ↾ { 𝐵 } ) ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
165 16 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ 𝐷 )
166 165 resmptd ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ↾ { 𝐵 } ) = ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) )
167 166 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ↾ { 𝐵 } ) ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
168 164 167 eqtr3d ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) )
169 168 fveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ 𝐷 ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ‘ 𝐴 ) = ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ‘ 𝐴 ) )
170 fveq1 ⊢ ( 𝑔 = 𝐴 → ( 𝑔 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑣 ) )
171 170 oveq2d ⊢ ( 𝑔 = 𝐴 → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) )
172 171 mpteq2dv ⊢ ( 𝑔 = 𝐴 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
173 172 oveq2d ⊢ ( 𝑔 = 𝐴 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
174 59 ringgrpd ⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Grp )
175 174 grpmndd ⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Mnd )
176 iftrue ⊢ ( 𝑠 = 𝐵 → if ( 𝑠 = 𝐵 , 1 , 0 ) = 1 )
177 110 a1i ⊢ ( 𝜑 → 1 ∈ V )
178 11 176 16 177 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = 1 )
179 178 fveq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 1 ) )
180 9 74 eqtr4id ⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑆 ) )
181 180 fveq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 1 ) = ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 1r ‘ 𝑆 ) ) )
182 sneq ⊢ ( 𝑥 = ( 1r ‘ 𝑆 ) → { 𝑥 } = { ( 1r ‘ 𝑆 ) } )
183 182 xpeq2d ⊢ ( 𝑥 = ( 1r ‘ 𝑆 ) → ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) = ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) )
184 snex ⊢ { ( 1r ‘ 𝑆 ) } ∈ V
185 184 a1i ⊢ ( 𝜑 → { ( 1r ‘ 𝑆 ) } ∈ V )
186 57 185 xpexd ⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) ∈ V )
187 48 183 76 186 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) )
188 181 187 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ 1 ) = ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) )
189 43 72 pws1 ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
190 56 57 189 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
191 179 188 190 3eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
192 191 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
193 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ CRing )
194 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
195 96 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 )
196 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑥 ∈ 𝐼 )
197 195 196 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐾 )
198 197 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
199 43 5 54 193 194 198 pwselbasr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
200 199 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
201 10 87 45 91 16 200 psrbagev2 ⊢ ( 𝜑 → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
202 eqid ⊢ ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
203 54 46 202 ringlidm ⊢ ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring ∧ ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) → ( ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
204 59 201 203 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
205 192 204 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
206 205 201 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
207 2fveq3 ⊢ ( 𝑏 = 𝐵 → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) )
208 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) )
209 208 oveq2d ⊢ ( 𝑏 = 𝐵 → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
210 207 209 oveq12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
211 54 210 gsumsn ⊢ ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Mnd ∧ 𝐵 ∈ 𝐷 ∧ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
212 175 16 206 211 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝐵 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
213 10 psrbagf ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 : 𝐼 ⟶ ℕ0 )
214 16 213 syl ⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ℕ0 )
215 214 ffnd ⊢ ( 𝜑 → 𝐵 Fn 𝐼 )
216 123 mptex ⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ V
217 216 49 fnmpti ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) Fn 𝐼
218 217 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) Fn 𝐼 )
219 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
220 eqidd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐵 ‘ 𝑣 ) = ( 𝐵 ‘ 𝑣 ) )
221 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑎 ‘ 𝑥 ) = ( 𝑎 ‘ 𝑣 ) )
222 221 mpteq2dv ⊢ ( 𝑥 = 𝑣 → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) )
223 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → 𝑣 ∈ 𝐼 )
224 123 mptex ⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ∈ V
225 224 a1i ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ∈ V )
226 49 222 223 225 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ‘ 𝑣 ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) )
227 215 218 12 12 219 220 226 offval ⊢ ( 𝜑 → ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) ) )
228 13 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → 𝑆 ∈ CRing )
229 ovexd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
230 44 ringmgp ⊢ ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ∈ Ring → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd )
231 59 230 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd )
232 231 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd )
233 214 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 )
234 96 adantl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 )
235 simplr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑣 ∈ 𝐼 )
236 234 235 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑣 ) ∈ 𝐾 )
237 236 fmpttd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
238 43 5 54 228 229 237 pwselbasr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
239 87 45 mulgnn0cl ⊢ ( ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ Mnd ∧ ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) → ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
240 232 233 238 239 syl3anc ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
241 43 5 54 228 229 240 pwselbas ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
242 241 ffnd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) Fn ( 𝐾 ↑m 𝐼 ) )
243 ovex ⊢ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ∈ V
244 eqid ⊢ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) )
245 243 244 fnmpti ⊢ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) Fn ( 𝐾 ↑m 𝐼 )
246 245 a1i ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) Fn ( 𝐾 ↑m 𝐼 ) )
247 eqid ⊢ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) )
248 fveq1 ⊢ ( 𝑎 = 𝑙 → ( 𝑎 ‘ 𝑣 ) = ( 𝑙 ‘ 𝑣 ) )
249 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) )
250 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑙 ‘ 𝑣 ) ∈ V )
251 247 248 249 250 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ‘ 𝑙 ) = ( 𝑙 ‘ 𝑣 ) )
252 251 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ‘ 𝑙 ) ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑙 ‘ 𝑣 ) ) )
253 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑆 ∈ Ring )
254 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
255 233 adantr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 )
256 238 adantr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
257 43 54 44 6 45 7 253 254 255 256 249 pwsexpg ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) ‘ 𝑙 ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ‘ 𝑙 ) ) )
258 fveq1 ⊢ ( 𝑔 = 𝑙 → ( 𝑔 ‘ 𝑣 ) = ( 𝑙 ‘ 𝑣 ) )
259 258 oveq2d ⊢ ( 𝑔 = 𝑙 → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑙 ‘ 𝑣 ) ) )
260 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑙 ‘ 𝑣 ) ) ∈ V )
261 244 259 249 260 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ‘ 𝑙 ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑙 ‘ 𝑣 ) ) )
262 252 257 261 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑙 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) ‘ 𝑙 ) = ( ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ‘ 𝑙 ) )
263 242 246 262 eqfnfvd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) )
264 263 mpteq2dva ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑣 ) ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) )
265 227 264 eqtrd ⊢ ( 𝜑 → ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) )
266 265 oveq2d ⊢ ( 𝜑 → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) ) )
267 6 crngmgp ⊢ ( 𝑆 ∈ CRing → 𝑀 ∈ CMnd )
268 13 267 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
269 268 cmnmndd ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
270 269 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑣 ∈ 𝐼 ) ) → 𝑀 ∈ Mnd )
271 233 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑣 ∈ 𝐼 ) ) → ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 )
272 elmapi ⊢ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ 𝐾 )
273 272 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑣 ∈ 𝐼 ) ) → 𝑔 : 𝐼 ⟶ 𝐾 )
274 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑣 ∈ 𝐼 ) ) → 𝑣 ∈ 𝐼 )
275 273 274 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑣 ∈ 𝐼 ) ) → ( 𝑔 ‘ 𝑣 ) ∈ 𝐾 )
276 6 5 mgpbas ⊢ 𝐾 = ( Base ‘ 𝑀 )
277 276 7 mulgnn0cl ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝐵 ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝑔 ‘ 𝑣 ) ∈ 𝐾 ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ∈ 𝐾 )
278 270 271 275 277 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑣 ∈ 𝐼 ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ∈ 𝐾 )
279 12 mptexd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) ∈ V )
280 fvexd ⊢ ( 𝜑 → ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∈ V )
281 funmpt ⊢ Fun ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) )
282 281 a1i ⊢ ( 𝜑 → Fun ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) )
283 10 psrbagfsupp ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 finSupp 0 )
284 16 283 syl ⊢ ( 𝜑 → 𝐵 finSupp 0 )
285 284 fsuppimpd ⊢ ( 𝜑 → ( 𝐵 supp 0 ) ∈ Fin )
286 ssidd ⊢ ( 𝜑 → ( 𝐵 supp 0 ) ⊆ ( 𝐵 supp 0 ) )
287 c0ex ⊢ 0 ∈ V
288 287 a1i ⊢ ( 𝜑 → 0 ∈ V )
289 214 286 12 288 suppssr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝐵 ‘ 𝑣 ) = 0 )
290 289 oveq1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) = ( 0 ↑ ( 𝑔 ‘ 𝑣 ) ) )
291 290 adantr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) ∧ 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) = ( 0 ↑ ( 𝑔 ‘ 𝑣 ) ) )
292 272 adantl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) ∧ 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑔 : 𝐼 ⟶ 𝐾 )
293 eldifi ⊢ ( 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) → 𝑣 ∈ 𝐼 )
294 293 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) ∧ 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑣 ∈ 𝐼 )
295 292 294 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) ∧ 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑔 ‘ 𝑣 ) ∈ 𝐾 )
296 6 72 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑀 )
297 276 296 7 mulg0 ⊢ ( ( 𝑔 ‘ 𝑣 ) ∈ 𝐾 → ( 0 ↑ ( 𝑔 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
298 295 297 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) ∧ 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 0 ↑ ( 𝑔 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
299 291 298 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) ∧ 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) = ( 1r ‘ 𝑆 ) )
300 299 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 1r ‘ 𝑆 ) ) )
301 fconstmpt ⊢ ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 1r ‘ 𝑆 ) )
302 ovexd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
303 56 302 189 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( ( 𝐾 ↑m 𝐼 ) × { ( 1r ‘ 𝑆 ) } ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
304 301 303 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
305 300 304 eqtrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝐼 ∖ ( 𝐵 supp 0 ) ) ) → ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) = ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
306 305 12 suppss2 ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) supp ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ⊆ ( 𝐵 supp 0 ) )
307 285 306 ssfid ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) supp ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ∈ Fin )
308 279 280 282 307 isfsuppd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) finSupp ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
309 43 5 202 44 6 57 12 13 278 308 pwsgprod ⊢ ( 𝜑 → ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) ) )
310 204 266 309 3eqtrd ⊢ ( 𝜑 → ( ( 1r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝐵 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) ) )
311 212 192 310 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝑔 ‘ 𝑣 ) ) ) ) ) )
312 ovexd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ V )
313 173 311 15 312 fvmptd4 ⊢ ( 𝜑 → ( ( ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ‘ ( 𝐹 ‘ 𝑏 ) ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) Σg ( 𝑏 ∘f ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ) ) ‘ 𝐴 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
314 53 169 313 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
315 37 314 jca ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )