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 may not be convenient. (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 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
39 1 2 4 3 10 5 6 7 38 12 13 14 37 15 evlsvvval ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) )
40 16 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ 𝐷 )
41 resmpt ⊢ ( { 𝐵 } ⊆ 𝐷 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) = ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
42 40 41 syl ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) = ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
43 42 oveq2d ⊢ ( 𝜑 → ( 𝑆 Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) ) = ( 𝑆 Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) )
44 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
45 13 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
46 45 ringcmnd ⊢ ( 𝜑 → 𝑆 ∈ CMnd )
47 45 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring )
48 3 subrgbas ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
49 5 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
50 48 49 eqsstrrd ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
51 14 50 syl ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
52 29 51 fssd ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐾 )
53 52 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 )
54 12 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
55 13 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing )
56 15 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
58 10 5 6 7 54 55 56 57 evlsvvvallem ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
59 5 38 47 53 58 ringcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ∈ 𝐾 )
60 59 fmpttd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) : 𝐷 ⟶ 𝐾 )
61 eldifsnneq ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) → ¬ 𝑏 = 𝐵 )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ¬ 𝑏 = 𝐵 )
63 62 iffalsed ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → if ( 𝑏 = 𝐵 , 1 , 0 ) = 0 )
64 eqeq1 ⊢ ( 𝑠 = 𝑏 → ( 𝑠 = 𝐵 ↔ 𝑏 = 𝐵 ) )
65 64 ifbid ⊢ ( 𝑠 = 𝑏 → if ( 𝑠 = 𝐵 , 1 , 0 ) = if ( 𝑏 = 𝐵 , 1 , 0 ) )
66 eldifi ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) → 𝑏 ∈ 𝐷 )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → 𝑏 ∈ 𝐷 )
68 9 fvexi ⊢ 1 ∈ V
69 8 fvexi ⊢ 0 ∈ V
70 68 69 ifex ⊢ if ( 𝑏 = 𝐵 , 1 , 0 ) ∈ V
71 70 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → if ( 𝑏 = 𝐵 , 1 , 0 ) ∈ V )
72 11 65 67 71 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑏 ) = if ( 𝑏 = 𝐵 , 1 , 0 ) )
73 3 44 subrg0 ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
74 73 8 eqtr4di ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = 0 )
75 14 74 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = 0 )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 0g ‘ 𝑆 ) = 0 )
77 63 72 76 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) )
78 77 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 0g ‘ 𝑆 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
79 66 58 sylan2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
80 5 38 44 ringlz ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 ) → ( ( 0g ‘ 𝑆 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
81 45 79 80 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 0g ‘ 𝑆 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
82 78 81 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0g ‘ 𝑆 ) )
83 82 19 suppss2 ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ { 𝐵 } )
84 10 2 3 4 5 6 7 38 12 13 14 37 15 evlsvvvallem2 ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑆 ) )
85 5 44 46 19 60 83 84 gsumres ⊢ ( 𝜑 → ( 𝑆 Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) )
86 13 crnggrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
87 86 grpmndd ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
88 52 16 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ 𝐾 )
89 10 5 6 7 12 13 15 16 evlsvvvallem ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
90 5 38 45 88 89 ringcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ∈ 𝐾 )
91 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
92 fveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑣 ) = ( 𝐵 ‘ 𝑣 ) )
93 92 oveq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) )
94 93 mpteq2dv ⊢ ( 𝑏 = 𝐵 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
95 94 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
96 91 95 oveq12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝐹 ‘ 𝐵 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
97 5 96 gsumsn ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝐵 ∈ 𝐷 ∧ ( ( 𝐹 ‘ 𝐵 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ∈ 𝐾 ) → ( 𝑆 Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( ( 𝐹 ‘ 𝐵 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
98 87 16 90 97 syl3anc ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( ( 𝐹 ‘ 𝐵 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
99 iftrue ⊢ ( 𝑠 = 𝐵 → if ( 𝑠 = 𝐵 , 1 , 0 ) = 1 )
100 68 a1i ⊢ ( 𝜑 → 1 ∈ V )
101 11 99 16 100 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = 1 )
102 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
103 3 102 subrg1 ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑈 ) )
104 14 103 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑈 ) )
105 9 101 104 3eqtr4a ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = ( 1r ‘ 𝑆 ) )
106 105 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
107 5 38 102 45 89 ringlidmd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
108 98 106 107 3eqtrd ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
109 43 85 108 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑆 ) ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
110 39 109 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
111 37 110 jca ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )