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 ffvelcdmda ⊢ ( ( ( ( 𝑁 ∈ 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 ffvelcdm ⊢ ( ( 𝑏 : ( 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 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
94 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
95 93 94 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
96 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
97 28 96 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
98 97 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
99 93 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
100 98 99 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
101 100 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
102 101 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
103 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
104 103 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
105 6 3 94 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
106 28 105 syl ⊢ ( 𝑅 ∈ CRing → 𝑋 ∈ ( Base ‘ 𝑃 ) )
107 106 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
108 107 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
109 108 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
110 95 7 102 104 109 mulgnn0cld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
111 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
112 111 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
113 112 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
114 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
115 113 114 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
116 115 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
117 116 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
118 117 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
119 118 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
120 119 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
121 110 120 mpbird ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
122 32 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
123 122 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑌 ∈ Ring )
124 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑁 ∈ Fin )
125 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
126 simpll3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑀 ∈ 𝐵 )
127 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
128 124 125 126 127 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
129 87 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → 𝑠 ∈ ℕ0 )
130 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
131 130 anim1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) )
132 1 2 3 4 5 m2pmfzmap ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
133 124 125 129 131 132 syl31anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
134 27 9 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
135 123 128 133 134 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
136 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
137 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
138 27 136 8 137 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
139 92 121 135 138 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
140 27 11 35 87 139 gsummptfzsplitl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
141 0nn0 ⊢ 0 ∈ ℕ0
142 141 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ℕ0 )
143 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
144 95 143 7 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
145 107 144 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
146 145 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
147 146 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
148 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
149 93 148 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
150 149 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) )
151 150 eqcomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) = ( 1r ‘ 𝑃 ) )
152 151 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0g ‘ ( mulGrp ‘ 𝑃 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
153 115 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
154 153 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1r ‘ 𝑃 ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) ) )
155 154 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
156 28 127 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
157 156 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
158 simpl ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ℕ ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
159 elnn0uz ⊢ ( 𝑠 ∈ ℕ0 ↔ 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
160 13 159 sylib ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
161 eluzfz1 ⊢ ( 𝑠 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑠 ) )
162 160 161 syl ⊢ ( 𝑠 ∈ ℕ → 0 ∈ ( 0 ... 𝑠 ) )
163 162 adantl ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ℕ ) → 0 ∈ ( 0 ... 𝑠 ) )
164 158 163 ffvelcdmd ⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑠 ∈ ℕ ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
165 164 ex ⊢ ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 → ( 𝑠 ∈ ℕ → ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
166 42 165 syl ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → ( 𝑠 ∈ ℕ → ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
167 166 impcom ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
168 167 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
169 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
170 60 40 168 169 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
171 27 9 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
172 122 157 170 171 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
173 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑌 ) ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) )
174 27 136 8 173 lmodvs1 ⊢ ( ( 𝑌 ∈ LMod ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
175 91 172 174 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
176 155 175 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
177 147 152 176 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
178 177 172 eqeltrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
179 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
180 2fveq3 ⊢ ( 𝑖 = 0 → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) )
181 180 oveq2d ⊢ ( 𝑖 = 0 → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
182 179 181 oveq12d ⊢ ( 𝑖 = 0 → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
183 182 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 = 0 ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
184 27 58 142 178 183 gsumsnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
185 95 149 7 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
186 107 185 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
187 186 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
188 187 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 1r ‘ 𝑃 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
189 184 188 176 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
190 189 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
191 140 190 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
192 86 191 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
193 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ... ( 𝑠 − 1 ) ) ∈ Fin )
194 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑁 ∈ Fin )
195 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑅 ∈ Ring )
196 42 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
197 196 adantr ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
198 nnz ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
199 fzoval ⊢ ( 𝑠 ∈ ℤ → ( 0 ..^ 𝑠 ) = ( 0 ... ( 𝑠 − 1 ) ) )
200 198 199 syl ⊢ ( 𝑠 ∈ ℕ → ( 0 ..^ 𝑠 ) = ( 0 ... ( 𝑠 − 1 ) ) )
201 200 eqcomd ⊢ ( 𝑠 ∈ ℕ → ( 0 ... ( 𝑠 − 1 ) ) = ( 0 ..^ 𝑠 ) )
202 201 eleq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↔ 𝑖 ∈ ( 0 ..^ 𝑠 ) ) )
203 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
204 202 203 biimtrdi ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
205 204 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
206 205 imp ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
207 197 206 ffvelcdmd ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
208 207 adantll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
209 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑖 ∈ ℕ0 )
210 209 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑖 ∈ ℕ0 )
211 50 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 1 ∈ ℕ0 )
212 210 211 nn0addcld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℕ0 )
213 194 195 208 212 53 syl22anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
214 213 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
215 27 35 193 214 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
216 27 11 cmncom ⊢ ( ( 𝑌 ∈ CMnd ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
217 35 215 71 216 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
218 217 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
219 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
220 32 219 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
221 220 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Grp )
222 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1 ... 𝑠 ) ∈ Fin )
223 91 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ LMod )
224 101 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
225 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ )
226 225 nnnn0d ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
227 226 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
228 108 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
229 95 7 224 227 228 mulgnn0cld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
230 115 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
231 230 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
232 231 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
233 229 232 eleqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
234 122 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ Ring )
235 157 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
236 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑁 ∈ Fin )
237 40 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑅 ∈ Ring )
238 196 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
239 238 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
240 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
241 fzss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝑠 ) ⊆ ( 0 ... 𝑠 ) )
242 240 241 mp1i ⊢ ( 𝑠 ∈ ℕ → ( 1 ... 𝑠 ) ⊆ ( 0 ... 𝑠 ) )
243 242 sseld ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
244 243 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) ) )
245 244 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
246 239 245 ffvelcdmd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 )
247 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 𝑖 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
248 236 237 246 247 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
249 234 235 248 134 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
250 223 233 249 138 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
251 250 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑠 ) ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
252 27 35 222 251 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
253 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 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) )
254 221 71 215 252 253 syl13anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) )
255 oveq1 ⊢ ( 𝑥 = 𝑖 → ( 𝑥 − 1 ) = ( 𝑖 − 1 ) )
256 255 oveq1d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑥 − 1 ) + 1 ) = ( ( 𝑖 − 1 ) + 1 ) )
257 256 oveq1d ⊢ ( 𝑥 = 𝑖 → ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) = ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) )
258 255 fveq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑏 ‘ ( 𝑥 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
259 258 fveq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
260 257 259 oveq12d ⊢ ( 𝑥 = 𝑖 → ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) = ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
261 260 cbvmptv ⊢ ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
262 225 nncnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℂ )
263 262 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℂ )
264 npcan1 ⊢ ( 𝑖 ∈ ℂ → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
265 263 264 syl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
266 265 oveq1d ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) = ( 𝑖 ↑ 𝑋 ) )
267 266 oveq1d ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
268 267 mpteq2dva ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑖 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) )
269 261 268 eqtrid ⊢ ( 𝑠 ∈ ℕ → ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) )
270 269 oveq2d ⊢ ( 𝑠 ∈ ℕ → ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) )
271 270 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) )
272 271 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
273 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
274 1zzd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 1 ∈ ℤ )
275 0zd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ℤ )
276 37 nn0zd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 − 1 ) ∈ ℤ )
277 oveq1 ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( 𝑖 + 1 ) = ( ( 𝑥 − 1 ) + 1 ) )
278 277 oveq1d ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( ( 𝑖 + 1 ) ↑ 𝑋 ) = ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) )
279 2fveq3 ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) )
280 278 279 oveq12d ⊢ ( 𝑖 = ( 𝑥 − 1 ) → ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) )
281 27 273 35 274 275 276 213 280 gsummptshft ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑥 ∈ ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) )
282 0p1e1 ⊢ ( 0 + 1 ) = 1
283 282 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 + 1 ) = 1 )
284 76 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑠 − 1 ) + 1 ) = 𝑠 )
285 283 284 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) = ( 1 ... 𝑠 ) )
286 285 mpteq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑥 ∈ ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) = ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) )
287 286 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑥 ∈ ( ( 0 + 1 ) ... ( ( 𝑠 − 1 ) + 1 ) ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) )
288 281 287 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) )
289 288 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑥 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( ( 𝑥 − 1 ) + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑥 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
290 ringabl ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Abel )
291 32 290 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Abel )
292 291 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Abel )
293 225 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℕ )
294 nnz ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℤ )
295 elfzm1b ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↔ ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) ) )
296 294 198 295 syl2an ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↔ ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) ) )
297 200 adantl ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 0 ..^ 𝑠 ) = ( 0 ... ( 𝑠 − 1 ) ) )
298 297 eqcomd ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 0 ... ( 𝑠 − 1 ) ) = ( 0 ..^ 𝑠 ) )
299 298 eleq2d ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) ↔ ( 𝑖 − 1 ) ∈ ( 0 ..^ 𝑠 ) ) )
300 elfzofz ⊢ ( ( 𝑖 − 1 ) ∈ ( 0 ..^ 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
301 299 300 biimtrdi ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑖 − 1 ) ∈ ( 0 ... ( 𝑠 − 1 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
302 296 301 sylbid ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
303 302 expimpd ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
304 293 303 mpcom ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
305 304 ex ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
306 305 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
307 306 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
308 239 307 ffvelcdmd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 )
309 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ∧ 𝑖 ∈ ℕ0 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
310 236 237 308 227 309 syl22anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
311 eqid ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
312 eqid ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
313 27 12 292 222 310 250 311 312 gsummptfidmsub ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
314 272 289 313 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
315 314 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) )
316 221 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ Grp )
317 27 12 grpsubcl ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
318 316 310 250 317 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
319 318 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑠 ) ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
320 27 35 222 319 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
321 27 11 cmncom ⊢ ( ( 𝑌 ∈ CMnd ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
322 35 71 320 321 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
323 254 315 322 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
324 323 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
325 27 11 mndcl ⊢ ( ( 𝑌 ∈ Mnd ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
326 58 71 215 325 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
327 27 11 12 292 326 252 172 ablsubsub4 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
328 27 11 12 grpaddsubass ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
329 221 320 71 172 328 syl13anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
330 324 327 329 3eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
331 5 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
332 236 237 308 331 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
333 27 8 136 137 12 223 233 332 249 lmodsubdi ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
334 333 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
335 334 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
336 335 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
337 336 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
338 218 330 337 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) ↦ ( ( ( 𝑖 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) − ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
339 18 192 338 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )