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