Metamath Proof Explorer

Theorem cpmadugsumlemF

Description: Lemma F for cpmadugsum . (Contributed by AV, 7-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cpmadugsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cpmadugsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmadugsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cpmadugsum.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cpmadugsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
cpmadugsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
cpmadugsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
cpmadugsum.r ⊢ × = ( .r ‘ 𝑌 )
cpmadugsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
cpmadugsum.g ⊢ + = ( +g ‘ 𝑌 )
cpmadugsum.s ⊢ − = ( -g ‘ 𝑌 )
Assertion cpmadugsumlemF ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cpmadugsum.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cpmadugsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cpmadugsum.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cpmadugsum.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6 cpmadugsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 cpmadugsum.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
8 cpmadugsum.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
9 cpmadugsum.r ⊢ × = ( .r ‘ 𝑌 )
10 cpmadugsum.1 ⊢ 1 = ( 1r ‘ 𝑌 )
11 cpmadugsum.g ⊢ + = ( +g ‘ 𝑌 )
12 cpmadugsum.s ⊢ − = ( -g ‘ 𝑌 )
13 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
14 1 2 3 4 5 6 7 8 9 10 cpmadugsumlemB ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
15 13 14 sylanr1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
16 1 2 3 4 5 6 7 8 9 10 cpmadugsumlemC ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
17 13 16 sylanr1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
18 15 17 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
19 nncn ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
20 npcan1 ⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 − 1 ) + 1 ) = 𝑠 )
21 20 eqcomd ⊢ ( 𝑠 ∈ ℂ → 𝑠 = ( ( 𝑠 − 1 ) + 1 ) )
22 19 21 syl ⊢ ( 𝑠 ∈ ℕ → 𝑠 = ( ( 𝑠 − 1 ) + 1 ) )
23 22 oveq2d ⊢ ( 𝑠 ∈ ℕ → ( 0 ... 𝑠 ) = ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) )
24 23 mpteq1d ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
25 24 oveq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
26 25 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
27 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
28 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
29 28 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
30 29 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
31 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
32 30 31 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
33 ringcmn ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ CMnd )
34 32 33 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ CMnd )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ CMnd )
36 nnm1nn0 ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 − 1 ) ∈ ℕ0 )
37 36 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 − 1 ) ∈ ℕ0 )
38 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → 𝑁 ∈ Fin )
39 28 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
40 39 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
41 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → 𝑅 ∈ Ring )
42 elmapi ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
43 23 feq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ↔ 𝑏 : ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ⟶ 𝐵 ) )
44 42 43 syl5ibcom ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → ( 𝑠 ∈ ℕ → 𝑏 : ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ⟶ 𝐵 ) )
45 44 impcom ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ⟶ 𝐵 )
46 45 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ⟶ 𝐵 )
47 46 ffvelrnda ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
48 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) → 𝑖 ∈ ℕ0 )
49 48 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → 𝑖 ∈ ℕ0 )
50 1nn0 ⊢ 1 ∈ ℕ0
51 50 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → 1 ∈ ℕ0 )
52 49 51 nn0addcld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℕ0 )
53 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 ∧ ( 𝑖 + 1 ) ∈ ℕ0 ) ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
54 38 41 47 52 53 syl22anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
55 27 11 35 37 54 gsummptfzsplit ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { ( ( 𝑠 − 1 ) + 1 ) } ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
56 ringmnd ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Mnd )
57 32 56 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Mnd )
58 57 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Mnd )
59 ovexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑠 − 1 ) + 1 ) ∈ V )
60 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
61 nn0fz0 ⊢ ( 𝑠 ∈ ℕ0 ↔ 𝑠 ∈ ( 0 ... 𝑠 ) )
62 13 61 sylib ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( 0 ... 𝑠 ) )
63 ffvelrn ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 )
64 42 62 63 syl2anr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 )
65 13 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
66 50 a1i ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 1 ∈ ℕ0 )
67 65 66 nn0addcld ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑠 + 1 ) ∈ ℕ0 )
68 64 67 jca ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 ∧ ( 𝑠 + 1 ) ∈ ℕ0 ) )
69 68 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 ∧ ( 𝑠 + 1 ) ∈ ℕ0 ) )
70 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 ∧ ( 𝑠 + 1 ) ∈ ℕ0 ) ) → ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) )
71 60 40 69 70 syl21anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) )
72 oveq1 ⊢ ( 𝑖 = ( ( 𝑠 − 1 ) + 1 ) → ( 𝑖 + 1 ) = ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) )
73 72 oveq1d ⊢ ( 𝑖 = ( ( 𝑠 − 1 ) + 1 ) → ( ( 𝑖 + 1 ) ↑ 𝑋 ) = ( ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) ↑ 𝑋 ) )
74 2fveq3 ⊢ ( 𝑖 = ( ( 𝑠 − 1 ) + 1 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 − 1 ) + 1 ) ) ) )
75 73 74 oveq12d ⊢ ( 𝑖 = ( ( 𝑠 − 1 ) + 1 ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 − 1 ) + 1 ) ) ) ) )
76 19 20 syl ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 − 1 ) + 1 ) = 𝑠 )
77 76 oveq1d ⊢ ( 𝑠 ∈ ℕ → ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) = ( 𝑠 + 1 ) )
78 77 oveq1d ⊢ ( 𝑠 ∈ ℕ → ( ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) ↑ 𝑋 ) = ( ( 𝑠 + 1 ) ↑ 𝑋 ) )
79 76 fveq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑏 ‘ ( ( 𝑠 − 1 ) + 1 ) ) = ( 𝑏 ‘ 𝑠 ) )
80 79 fveq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 − 1 ) + 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
81 78 80 oveq12d ⊢ ( 𝑠 ∈ ℕ → ( ( ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 − 1 ) + 1 ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
82 81 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 − 1 ) + 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 − 1 ) + 1 ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
83 75 82 sylan9eqr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 = ( ( 𝑠 − 1 ) + 1 ) ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
84 27 58 59 71 83 gsumsnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { ( ( 𝑠 − 1 ) + 1 ) } ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
85 84 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { ( ( 𝑠 − 1 ) + 1 ) } ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
86 26 55 85 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
87 13 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℕ0 )
88 3 4 pmatlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
89 29 88 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
90 89 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ LMod )
91 90 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ LMod )
92 91 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ LMod )
93 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
94 28 93 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
95 94 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
96 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
97 96 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
98 95 97 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
99 98 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
100 99 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
101 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
102 101 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
103 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
104 6 3 103 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
105 28 104 syl ⊢ ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ 𝑃 ) )
106 105 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
107 106 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
108 107 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
109 96 103 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
110 109 7 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑖 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
111 100 102 108 110 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
112 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
113 112 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
114 113 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
115 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
116 114 115 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
117 116 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
118 117 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
119 118 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
120 119 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
121 120 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
122 111 121 mpbird ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
123 32 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
124 123 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ Ring )
125 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑁 ∈ Fin )
126 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
127 simpll3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑀 ∈ 𝐵 )
128 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
129 125 126 127 128 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
130 87 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑠 ∈ ℕ0 )
131 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
132 131 anim1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) )
133 1 2 3 4 5 m2pmfzmap ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
134 125 126 130 132 133 syl31anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
135 27 9 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
136 124 129 134 135 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
137 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
138 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
139 27 137 8 138 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
140 92 122 136 139 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
141 27 11 35 87 140 gsummptfzsplitl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
142 0nn0 ⊢ 0 ∈ ℕ0
143 142 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ℕ0 )
144 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
145 109 144 7 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
146 106 145 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
147 146 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
148 147 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
149 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
150 96 149 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
151 150 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
152 151 eqcomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) = ( 1r ‘ 𝑃 ) )
153 152 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
154 116 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
155 154 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1r ‘ 𝑃 ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) ) )
156 155 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
157 28 128 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
158 157 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
159 simpl ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ℕ ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
160 elnn0uz ⊢ ( 𝑠 ∈ ℕ0 ↔ 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
161 13 160 sylib ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
162 eluzfz1 ⊢ ( 𝑠 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑠 ) )
163 161 162 syl ⊢ ( 𝑠 ∈ ℕ → 0 ∈ ( 0 ... 𝑠 ) )
164 163 adantl ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ℕ ) → 0 ∈ ( 0 ... 𝑠 ) )
165 159 164 ffvelrnd ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ℕ ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
166 165 ex ⊢ ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 → ( 𝑠 ∈ ℕ → ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
167 42 166 syl ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → ( 𝑠 ∈ ℕ → ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
168 167 impcom ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
169 168 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
170 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
171 60 40 169 170 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
172 27 9 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
173 123 158 171 172 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
174 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑌 ) ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) )
175 27 137 8 174 lmodvs1 ⊢ ( ( 𝑌 ∈ LMod ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
176 91 173 175 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
177 156 176 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
178 148 153 177 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
179 178 173 eqeltrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
180 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
181 2fveq3 ⊢ ( 𝑖 = 0 → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) )
182 181 oveq2d ⊢ ( 𝑖 = 0 → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
183 180 182 oveq12d ⊢ ( 𝑖 = 0 → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
184 183 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 = 0 ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
185 27 58 143 179 184 gsumsnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
186 109 150 7 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
187 106 186 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
188 187 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
189 188 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
190 185 189 177 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
191 190 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
192 141 191 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
193 86 192 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
194 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ... ( 𝑠 − 1 ) ) ∈ Fin )
195 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑁 ∈ Fin )
196 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑅 ∈ Ring )
197 42 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
198 197 adantr ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
199 nnz ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
200 fzoval ⊢ ( 𝑠 ∈ ℤ → ( 0 ..^ 𝑠 ) = ( 0 ... ( 𝑠 − 1 ) ) )
201 199 200 syl ⊢ ( 𝑠 ∈ ℕ → ( 0 ..^ 𝑠 ) = ( 0 ... ( 𝑠 − 1 ) ) )
202 201 eqcomd ⊢ ( 𝑠 ∈ ℕ → ( 0 ... ( 𝑠 − 1 ) ) = ( 0 ..^ 𝑠 ) )
203 202 eleq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↔ 𝑖 ∈ ( 0 ..^ 𝑠 ) ) )
204 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
205 203 204 syl6bi ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
206 205 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
207 206 imp ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
208 198 207 ffvelrnd ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
209 208 adantll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
210 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑖 ∈ ℕ0 )
211 210 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑖 ∈ ℕ0 )
212 50 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 1 ∈ ℕ0 )
213 211 212 nn0addcld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℕ0 )
214 195 196 209 213 53 syl22anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
215 214 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
216 27 35 194 215 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
217 27 11 cmncom ⊢ ( ( 𝑌 ∈ CMnd ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
218 35 216 71 217 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
219 218 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
220 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
221 32 220 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
222 221 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Grp )
223 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1 ... 𝑠 ) ∈ Fin )
224 91 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ LMod )
225 99 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
226 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ )
227 226 nnnn0d ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
228 227 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
229 107 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
230 225 228 229 110 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
231 116 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
232 231 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
233 232 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
234 230 233 eleqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
235 123 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ Ring )
236 158 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
237 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑁 ∈ Fin )
238 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑅 ∈ Ring )
239 197 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
240 239 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
241 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
242 fzss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝑠 ) ⊆ ( 0 ... 𝑠 ) )
243 241 242 mp1i ⊢ ( 𝑠 ∈ ℕ → ( 1 ... 𝑠 ) ⊆ ( 0 ... 𝑠 ) )
244 243 sseld ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
245 244 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
246 245 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
247 240 246 ffvelrnd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
248 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
249 237 238 247 248 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
250 235 236 249 135 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
251 224 234 250 139 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
252 251 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑠 ) ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
253 27 35 223 252 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
254 27 11 12 grpaddsubass ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) )
255 222 71 216 253 254 syl13anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) )
256 oveq1 ⊢ ( 𝑥 = 𝑖 → ( 𝑥 − 1 ) = ( 𝑖 − 1 ) )
257 256 oveq1d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑥 − 1 ) + 1 ) = ( ( 𝑖 − 1 ) + 1 ) )
258 257 oveq1d ⊢ ( 𝑥 = 𝑖 → ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) = ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) )
259 256 fveq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑏 ‘ ( 𝑥 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
260 259 fveq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
261 258 260 oveq12d ⊢ ( 𝑥 = 𝑖 → ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) = ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
262 261 cbvmptv ⊢ ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
263 226 nncnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℂ )
264 263 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℂ )
265 npcan1 ⊢ ( 𝑖 ∈ ℂ → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
266 264 265 syl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
267 266 oveq1d ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) = ( 𝑖 ↑ 𝑋 ) )
268 267 oveq1d ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
269 268 mpteq2dva ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) )
270 262 269 syl5eq ⊢ ( 𝑠 ∈ ℕ → ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) )
271 270 oveq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) )
272 271 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) )
273 272 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
274 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
275 1zzd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 1 ∈ ℤ )
276 0zd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ℤ )
277 37 nn0zd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 − 1 ) ∈ ℤ )
278 oveq1 ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( 𝑖 + 1 ) = ( ( 𝑥 − 1 ) + 1 ) )
279 278 oveq1d ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( ( 𝑖 + 1 ) ↑ 𝑋 ) = ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) )
280 2fveq3 ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) )
281 279 280 oveq12d ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) )
282 27 274 35 275 276 277 214 281 gsummptshft ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑥 ∈ ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) )
283 0p1e1 ⊢ ( 0 + 1 ) = 1
284 283 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 + 1 ) = 1 )
285 76 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑠 − 1 ) + 1 ) = 𝑠 )
286 284 285 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) = ( 1 ... 𝑠 ) )
287 286 mpteq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑥 ∈ ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) )
288 287 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑥 ∈ ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) )
289 282 288 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) )
290 289 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
291 ringabl ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Abel )
292 32 291 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Abel )
293 292 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Abel )
294 226 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℕ )
295 nnz ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℤ )
296 elfzm1b ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↔ ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) ) )
297 295 199 296 syl2an ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↔ ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) ) )
298 201 adantl ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 0 ..^ 𝑠 ) = ( 0 ... ( 𝑠 − 1 ) ) )
299 298 eqcomd ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 0 ... ( 𝑠 − 1 ) ) = ( 0 ..^ 𝑠 ) )
300 299 eleq2d ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) ↔ ( 𝑖 − 1 ) ∈ ( 0 ..^ 𝑠 ) ) )
301 elfzofz ⊢ ( ( 𝑖 − 1 ) ∈ ( 0 ..^ 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
302 300 301 syl6bi ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
303 297 302 sylbid ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
304 303 expimpd ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
305 294 304 mpcom ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
306 305 ex ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
307 306 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
308 307 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
309 240 308 ffvelrnd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 )
310 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ∧ 𝑖 ∈ ℕ0 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
311 237 238 309 228 310 syl22anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
312 eqid ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
313 eqid ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
314 27 12 293 223 311 251 312 313 gsummptfidmsub ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
315 273 290 314 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
316 315 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) )
317 222 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ Grp )
318 27 12 grpsubcl ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
319 317 311 251 318 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
320 319 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑠 ) ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
321 27 35 223 320 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
322 27 11 cmncom ⊢ ( ( 𝑌 ∈ CMnd ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
323 35 71 321 322 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
324 255 316 323 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
325 324 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
326 27 11 mndcl ⊢ ( ( 𝑌 ∈ Mnd ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
327 58 71 216 326 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
328 27 11 12 293 327 253 173 ablsubsub4 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
329 27 11 12 grpaddsubass ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
330 222 321 71 173 329 syl13anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
331 325 328 330 3eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
332 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
333 237 238 309 332 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
334 27 8 137 138 12 224 234 333 250 lmodsubdi ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
335 334 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
336 335 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
337 336 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
338 337 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
339 219 331 338 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
340 18 193 339 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )