Metamath Proof Explorer

Theorem chfacfpmmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019)

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

Proof

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