Metamath Proof Explorer

Theorem chfacfscmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 chfacfisf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 chfacfisf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 chfacfisf.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 chfacfisf.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 chfacfisf.r ⊢ × = ( .r ‘ 𝑌 )
6 chfacfisf.s ⊢ − = ( -g ‘ 𝑌 )
7 chfacfisf.0 ⊢ 0 = ( 0g ‘ 𝑌 )
8 chfacfisf.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9 chfacfisf.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10 chfacfscmulcl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
11 chfacfscmulcl.m ⊢ · = ( ·𝑠 ‘ 𝑌 )
12 chfacfscmulcl.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
13 chfacfscmulgsum.p ⊢ + = ( +g ‘ 𝑌 )
14 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
15 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16 15 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
17 16 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
18 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
19 17 18 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
20 ringcmn ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ CMnd )
21 19 20 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ CMnd )
22 21 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ CMnd )
23 nn0ex ⊢ ℕ0 ∈ V
24 23 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ℕ0 ∈ V )
25 simpll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) )
26 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) )
27 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
28 25 26 27 3jca ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ℕ0 ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
30 28 29 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
31 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulfsupp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) finSupp 0 )
32 nn0disj ⊢ ( ( 0 ... ( 𝑠 + 1 ) ) ∩ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) = ∅
33 32 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ... ( 𝑠 + 1 ) ) ∩ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) = ∅ )
34 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
35 peano2nn0 ⊢ ( 𝑠 ∈ ℕ0 → ( 𝑠 + 1 ) ∈ ℕ0 )
36 34 35 syl ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℕ0 )
37 nn0split ⊢ ( ( 𝑠 + 1 ) ∈ ℕ0 → ℕ0 = ( ( 0 ... ( 𝑠 + 1 ) ) ∪ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) )
38 36 37 syl ⊢ ( 𝑠 ∈ ℕ → ℕ0 = ( ( 0 ... ( 𝑠 + 1 ) ) ∪ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) )
39 38 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ℕ0 = ( ( 0 ... ( 𝑠 + 1 ) ) ∪ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) )
40 14 7 13 22 24 30 31 33 39 gsumsplit2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
41 simpll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) )
42 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) → ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) )
43 nncn ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
44 add1p1 ⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
45 43 44 syl ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
46 45 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
47 46 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) = ( ℤ≥ ‘ ( 𝑠 + 2 ) ) )
48 47 eleq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↔ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) )
49 48 biimpa ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmul0 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 )
51 41 42 49 50 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = 0 )
52 51 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ 0 ) )
53 52 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ 0 ) ) )
54 15 18 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
55 ringmnd ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Mnd )
56 54 55 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Mnd )
57 56 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Mnd )
58 fvex ⊢ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ∈ V
59 57 58 jctir ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑌 ∈ Mnd ∧ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ∈ V ) )
60 59 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 ∈ Mnd ∧ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ∈ V ) )
61 7 gsumz ⊢ ( ( 𝑌 ∈ Mnd ∧ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ∈ V ) → ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ 0 ) ) = 0 )
62 60 61 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ 0 ) ) = 0 )
63 53 62 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = 0 )
64 63 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + 0 ) )
65 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ... ( 𝑠 + 1 ) ) ∈ Fin )
66 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) → 𝑖 ∈ ℕ0 )
67 66 28 sylan2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑖 ∈ ℕ0 ) )
68 67 29 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
69 68 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
70 14 22 65 69 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
71 14 13 7 mndrid ⊢ ( ( 𝑌 ∈ Mnd ∧ ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + 0 ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
72 57 70 71 syl2an2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + 0 ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
73 64 72 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ ( ℤ≥ ‘ ( ( 𝑠 + 1 ) + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) )
74 34 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℕ0 )
75 14 13 22 74 68 gsummptfzsplit ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { ( 𝑠 + 1 ) } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
76 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
77 76 30 sylan2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
78 14 13 22 74 77 gsummptfzsplitl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) )
79 57 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Mnd )
80 0nn0 ⊢ 0 ∈ ℕ0
81 80 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ℕ0 )
82 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 0 ∈ ℕ0 ) → ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
83 81 82 mpd3an3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
84 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
85 fveq2 ⊢ ( 𝑖 = 0 → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 0 ) )
86 84 85 oveq12d ⊢ ( 𝑖 = 0 → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) )
87 14 86 gsumsn ⊢ ( ( 𝑌 ∈ Mnd ∧ 0 ∈ ℕ0 ∧ ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) )
88 79 81 83 87 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) )
89 88 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { 0 } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) )
90 78 89 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) )
91 ovexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ V )
92 1nn0 ⊢ 1 ∈ ℕ0
93 92 a1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 1 ∈ ℕ0 )
94 74 93 nn0addcld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℕ0 )
95 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ ( 𝑠 + 1 ) ∈ ℕ0 ) → ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
96 94 95 mpd3an3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
97 oveq1 ⊢ ( 𝑖 = ( 𝑠 + 1 ) → ( 𝑖 ↑ 𝑋 ) = ( ( 𝑠 + 1 ) ↑ 𝑋 ) )
98 fveq2 ⊢ ( 𝑖 = ( 𝑠 + 1 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝑠 + 1 ) ) )
99 97 98 oveq12d ⊢ ( 𝑖 = ( 𝑠 + 1 ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) )
100 14 99 gsumsn ⊢ ( ( 𝑌 ∈ Mnd ∧ ( 𝑠 + 1 ) ∈ V ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( 𝑌 Σg ( 𝑖 ∈ { ( 𝑠 + 1 ) } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) )
101 79 91 96 100 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ { ( 𝑠 + 1 ) } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) )
102 90 101 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( 𝑌 Σg ( 𝑖 ∈ { ( 𝑠 + 1 ) } ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) )
103 fzfid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1 ... 𝑠 ) ∈ Fin )
104 simpll ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) )
105 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) )
106 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ )
107 106 nnnn0d ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ0 )
108 107 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℕ0 )
109 104 105 108 29 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
110 109 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑠 ) ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
111 14 22 103 110 gsummptcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
112 14 13 mndass ⊢ ( ( 𝑌 ∈ Mnd ∧ ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) ) )
113 79 111 83 96 112 syl13anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) ) )
114 106 nnne0d ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ≠ 0 )
115 114 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑖 ≠ 0 )
116 neeq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ≠ 0 ↔ 𝑖 ≠ 0 ) )
117 116 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → ( 𝑛 ≠ 0 ↔ 𝑖 ≠ 0 ) )
118 115 117 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑛 ≠ 0 )
119 eqneqall ⊢ ( 𝑛 = 0 → ( 𝑛 ≠ 0 → 0 = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
120 118 119 mpan9 ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → 0 = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
121 simplr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → 𝑛 = 𝑖 )
122 eqeq1 ⊢ ( 0 = 𝑛 → ( 0 = 𝑖 ↔ 𝑛 = 𝑖 ) )
123 122 eqcoms ⊢ ( 𝑛 = 0 → ( 0 = 𝑖 ↔ 𝑛 = 𝑖 ) )
124 123 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → ( 0 = 𝑖 ↔ 𝑛 = 𝑖 ) )
125 121 124 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → 0 = 𝑖 )
126 125 fveq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → ( 𝑏 ‘ 0 ) = ( 𝑏 ‘ 𝑖 ) )
127 126 fveq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) )
128 127 oveq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
129 120 128 oveq12d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ 𝑛 = 0 ) → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
130 elfz2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠 ) ) )
131 zleltp1 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑖 ≤ 𝑠 ↔ 𝑖 < ( 𝑠 + 1 ) ) )
132 131 ancoms ⊢ ( ( 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ≤ 𝑠 ↔ 𝑖 < ( 𝑠 + 1 ) ) )
133 132 3adant1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ≤ 𝑠 ↔ 𝑖 < ( 𝑠 + 1 ) ) )
134 133 biimpcd ⊢ ( 𝑖 ≤ 𝑠 → ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 < ( 𝑠 + 1 ) ) )
135 134 adantl ⊢ ( ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠 ) → ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 < ( 𝑠 + 1 ) ) )
136 135 impcom ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠 ) ) → 𝑖 < ( 𝑠 + 1 ) )
137 136 orcd ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠 ) ) → ( 𝑖 < ( 𝑠 + 1 ) ∨ ( 𝑠 + 1 ) < 𝑖 ) )
138 zre ⊢ ( 𝑠 ∈ ℤ → 𝑠 ∈ ℝ )
139 1red ⊢ ( 𝑠 ∈ ℤ → 1 ∈ ℝ )
140 138 139 readdcld ⊢ ( 𝑠 ∈ ℤ → ( 𝑠 + 1 ) ∈ ℝ )
141 zre ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℝ )
142 140 141 anim12ci ⊢ ( ( 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ∈ ℝ ∧ ( 𝑠 + 1 ) ∈ ℝ ) )
143 142 3adant1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ∈ ℝ ∧ ( 𝑠 + 1 ) ∈ ℝ ) )
144 lttri2 ⊢ ( ( 𝑖 ∈ ℝ ∧ ( 𝑠 + 1 ) ∈ ℝ ) → ( 𝑖 ≠ ( 𝑠 + 1 ) ↔ ( 𝑖 < ( 𝑠 + 1 ) ∨ ( 𝑠 + 1 ) < 𝑖 ) ) )
145 143 144 syl ⊢ ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ≠ ( 𝑠 + 1 ) ↔ ( 𝑖 < ( 𝑠 + 1 ) ∨ ( 𝑠 + 1 ) < 𝑖 ) ) )
146 145 adantr ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠 ) ) → ( 𝑖 ≠ ( 𝑠 + 1 ) ↔ ( 𝑖 < ( 𝑠 + 1 ) ∨ ( 𝑠 + 1 ) < 𝑖 ) ) )
147 137 146 mpbird ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠 ) ) → 𝑖 ≠ ( 𝑠 + 1 ) )
148 130 147 sylbi ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ≠ ( 𝑠 + 1 ) )
149 148 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑖 ≠ ( 𝑠 + 1 ) )
150 neeq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ≠ ( 𝑠 + 1 ) ↔ 𝑖 ≠ ( 𝑠 + 1 ) ) )
151 150 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → ( 𝑛 ≠ ( 𝑠 + 1 ) ↔ 𝑖 ≠ ( 𝑠 + 1 ) ) )
152 149 151 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑛 ≠ ( 𝑠 + 1 ) )
153 152 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ≠ ( 𝑠 + 1 ) )
154 153 neneqd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) → ¬ 𝑛 = ( 𝑠 + 1 ) )
155 154 pm2.21d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑛 = ( 𝑠 + 1 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
156 155 imp ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 = ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
157 106 nnred ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℝ )
158 eleq1w ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ∈ ℝ ↔ 𝑖 ∈ ℝ ) )
159 157 158 syl5ibrcom ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑛 = 𝑖 → 𝑛 ∈ ℝ ) )
160 159 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑛 = 𝑖 → 𝑛 ∈ ℝ ) )
161 160 imp ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑛 ∈ ℝ )
162 74 nn0red ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℝ )
163 162 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑠 ∈ ℝ )
164 1red ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 1 ∈ ℝ )
165 163 164 readdcld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → ( 𝑠 + 1 ) ∈ ℝ )
166 130 136 sylbi ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 < ( 𝑠 + 1 ) )
167 166 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑖 < ( 𝑠 + 1 ) )
168 breq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 < ( 𝑠 + 1 ) ↔ 𝑖 < ( 𝑠 + 1 ) ) )
169 168 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → ( 𝑛 < ( 𝑠 + 1 ) ↔ 𝑖 < ( 𝑠 + 1 ) ) )
170 167 169 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → 𝑛 < ( 𝑠 + 1 ) )
171 161 165 170 ltnsymd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → ¬ ( 𝑠 + 1 ) < 𝑛 )
172 171 pm2.21d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → ( ( 𝑠 + 1 ) < 𝑛 → 0 = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
173 172 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) → ( ( 𝑠 + 1 ) < 𝑛 → 0 = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
174 173 imp ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ( 𝑠 + 1 ) < 𝑛 ) → 0 = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
175 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → 𝑛 = 𝑖 )
176 175 fvoveq1d ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( 𝑏 ‘ ( 𝑛 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
177 176 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
178 175 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( 𝑏 ‘ 𝑛 ) = ( 𝑏 ‘ 𝑖 ) )
179 178 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) )
180 179 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
181 177 180 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
182 174 181 ifeqda ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
183 156 182 ifeqda ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) ∧ ¬ 𝑛 = 0 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
184 129 183 ifeqda ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) ∧ 𝑛 = 𝑖 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
185 ovexd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ∈ V )
186 9 184 108 185 fvmptd2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝐺 ‘ 𝑖 ) = ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
187 186 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
188 187 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
189 188 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
190 nn0p1gt0 ⊢ ( 𝑠 ∈ ℕ0 → 0 < ( 𝑠 + 1 ) )
191 0red ⊢ ( 𝑠 ∈ ℕ0 → 0 ∈ ℝ )
192 ltne ⊢ ( ( 0 ∈ ℝ ∧ 0 < ( 𝑠 + 1 ) ) → ( 𝑠 + 1 ) ≠ 0 )
193 191 192 sylan ⊢ ( ( 𝑠 ∈ ℕ0 ∧ 0 < ( 𝑠 + 1 ) ) → ( 𝑠 + 1 ) ≠ 0 )
194 neeq1 ⊢ ( 𝑛 = ( 𝑠 + 1 ) → ( 𝑛 ≠ 0 ↔ ( 𝑠 + 1 ) ≠ 0 ) )
195 193 194 syl5ibrcom ⊢ ( ( 𝑠 ∈ ℕ0 ∧ 0 < ( 𝑠 + 1 ) ) → ( 𝑛 = ( 𝑠 + 1 ) → 𝑛 ≠ 0 ) )
196 34 190 195 syl2anc2 ⊢ ( 𝑠 ∈ ℕ → ( 𝑛 = ( 𝑠 + 1 ) → 𝑛 ≠ 0 ) )
197 196 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 = ( 𝑠 + 1 ) → 𝑛 ≠ 0 ) )
198 197 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 = ( 𝑠 + 1 ) ) → 𝑛 ≠ 0 )
199 eqneqall ⊢ ( 𝑛 = 0 → ( 𝑛 ≠ 0 → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
200 198 199 mpan9 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 = ( 𝑠 + 1 ) ) ∧ 𝑛 = 0 ) → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
201 iftrue ⊢ ( 𝑛 = ( 𝑠 + 1 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
202 201 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ 𝑛 = 0 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
203 200 202 ifeqda ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 = ( 𝑠 + 1 ) ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
204 74 35 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℕ0 )
205 fvexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ V )
206 9 203 204 205 fvmptd2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐺 ‘ ( 𝑠 + 1 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
207 206 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) = ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
208 15 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
209 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
210 10 3 209 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
211 208 210 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
212 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
213 212 209 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
214 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
215 212 214 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
216 213 215 12 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
217 211 216 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
218 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
219 218 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
220 219 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
221 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
222 220 221 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
223 222 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 1r ‘ 𝑃 ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) ) )
224 217 223 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) ) )
225 224 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) ) )
226 225 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( 𝐺 ‘ 0 ) ) )
227 3 4 pmatlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
228 15 227 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
229 228 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ LMod )
230 1 2 3 4 5 6 7 8 9 chfacfisf ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
231 15 230 syl3anl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
232 231 81 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐺 ‘ 0 ) ∈ ( Base ‘ 𝑌 ) )
233 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
234 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑌 ) ) = ( 1r ‘ ( Scalar ‘ 𝑌 ) )
235 14 233 11 234 lmodvs1 ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐺 ‘ 0 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( 𝐺 ‘ 0 ) ) = ( 𝐺 ‘ 0 ) )
236 229 232 235 syl2an2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑌 ) ) · ( 𝐺 ‘ 0 ) ) = ( 𝐺 ‘ 0 ) )
237 iftrue ⊢ ( 𝑛 = 0 → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
238 ovexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ V )
239 9 237 81 238 fvmptd3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐺 ‘ 0 ) = ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
240 226 236 239 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) = ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
241 207 240 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
242 14 13 cmncom ⊢ ( ( 𝑌 ∈ CMnd ∧ ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) )
243 22 83 96 242 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) )
244 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
245 19 244 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
246 245 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Grp )
247 207 96 eqeltrrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) )
248 19 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
249 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
250 15 249 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
251 250 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
252 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
253 208 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
254 elmapi ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
255 254 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
256 255 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
257 0elfz ⊢ ( 𝑠 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑠 ) )
258 34 257 syl ⊢ ( 𝑠 ∈ ℕ → 0 ∈ ( 0 ... 𝑠 ) )
259 258 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ( 0 ... 𝑠 ) )
260 256 259 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
261 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
262 252 253 260 261 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
263 14 5 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
264 248 251 262 263 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
265 14 7 6 13 grpsubadd0sub ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
266 246 247 264 265 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) + ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
267 241 243 266 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) = ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) )
268 189 267 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
269 113 268 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) + ( ( 0 ↑ 𝑋 ) · ( 𝐺 ‘ 0 ) ) ) + ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝐺 ‘ ( 𝑠 + 1 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
270 75 102 269 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... ( 𝑠 + 1 ) ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
271 40 73 270 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )