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 syl6bi ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 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 syl6bi ( ( 𝑖 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑖 − 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 ) ) ) ) ) )