Metamath Proof Explorer

Theorem cayhamlem1

Description: Lemma 1 for cayleyhamilton . (Contributed by AV, 11-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 ‘ 𝑌 ) )
Assertion cayhamlem1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑖 ) ) ) ) = 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 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
12 1 2 3 4 5 6 7 8 9 10 11 chfacfpmmulgsum2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
13 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℤ )
14 13 zcnd ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℂ )
15 pncan1 ⊢ ( 𝑖 ∈ ℂ → ( ( 𝑖 + 1 ) − 1 ) = 𝑖 )
16 14 15 syl ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( ( 𝑖 + 1 ) − 1 ) = 𝑖 )
17 16 eqcomd ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 = ( ( 𝑖 + 1 ) − 1 ) )
18 17 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 = ( ( 𝑖 + 1 ) − 1 ) )
19 18 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ‘ 𝑖 ) = ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) )
20 19 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) )
21 20 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) )
22 21 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) ) )
23 22 mpteq2dva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) ) ) )
24 23 oveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) ) ) ) )
25 24 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) ) ) ) )
26 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
27 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
28 27 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
29 28 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
30 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
31 29 30 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
32 ringabl ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Abel )
33 31 32 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Abel )
34 33 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Abel )
35 elnnuz ⊢ ( 𝑠 ∈ ℕ ↔ 𝑠 ∈ ( ℤ≥ ‘ 1 ) )
36 35 biimpi ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( ℤ≥ ‘ 1 ) )
37 36 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ( ℤ≥ ‘ 1 ) )
38 31 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
39 38 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → 𝑌 ∈ Ring )
40 28 30 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
41 40 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
42 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
43 42 ringmgp ⊢ ( 𝑌 ∈ Ring → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
44 41 43 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
45 44 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
46 45 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
47 mndmgm ⊢ ( ( mulGrp ‘ 𝑌 ) ∈ Mnd → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
48 46 47 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
49 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → 𝑘 ∈ ℕ )
50 49 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → 𝑘 ∈ ℕ )
51 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
52 27 51 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
53 52 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
54 53 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
55 42 26 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
56 55 10 mulgnncl ⊢ ( ( ( mulGrp ‘ 𝑌 ) ∈ Mgm ∧ 𝑘 ∈ ℕ ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) → ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
57 48 50 54 56 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
58 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
59 58 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → 𝑁 ∈ Fin )
60 27 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
61 60 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
62 61 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → 𝑅 ∈ Ring )
63 elmapi ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
64 63 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
65 64 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
66 65 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
67 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
68 peano2nn ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℕ )
69 68 nnzd ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℤ )
70 elfzm1b ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑠 + 1 ) ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ↔ ( 𝑘 − 1 ) ∈ ( 0 ... ( ( 𝑠 + 1 ) − 1 ) ) ) )
71 67 69 70 syl2an ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ↔ ( 𝑘 − 1 ) ∈ ( 0 ... ( ( 𝑠 + 1 ) − 1 ) ) ) )
72 nncn ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
73 pncan1 ⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 + 1 ) − 1 ) = 𝑠 )
74 72 73 syl ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 1 ) − 1 ) = 𝑠 )
75 74 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) − 1 ) = 𝑠 )
76 75 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 0 ... ( ( 𝑠 + 1 ) − 1 ) ) = ( 0 ... 𝑠 ) )
77 76 eleq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑘 − 1 ) ∈ ( 0 ... ( ( 𝑠 + 1 ) − 1 ) ) ↔ ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
78 77 biimpd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑘 − 1 ) ∈ ( 0 ... ( ( 𝑠 + 1 ) − 1 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
79 71 78 sylbid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ ) → ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
80 79 expcom ⊢ ( 𝑠 ∈ ℕ → ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) ) )
81 80 com13 ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → ( 𝑘 ∈ ℕ → ( 𝑠 ∈ ℕ → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) ) )
82 49 81 mpd ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → ( 𝑠 ∈ ℕ → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
83 82 com12 ⊢ ( 𝑠 ∈ ℕ → ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
84 83 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
85 84 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... 𝑠 ) )
86 66 85 ffvelcdmd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ 𝐵 )
87 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
88 59 62 86 87 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
89 26 5 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
90 39 57 88 89 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ) → ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
91 90 ralrimiva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ... ( 𝑠 + 1 ) ) ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
92 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) )
93 fvoveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
94 93 fveq2d ⊢ ( 𝑘 = 𝑖 → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
95 92 94 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
96 oveq1 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) )
97 fvoveq1 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) = ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) )
98 97 fveq2d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) )
99 96 98 oveq12d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) = ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) )
100 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) )
101 fvoveq1 ⊢ ( 𝑘 = 1 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) = ( 𝑏 ‘ ( 1 − 1 ) ) )
102 101 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) )
103 100 102 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) = ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) )
104 oveq1 ⊢ ( 𝑘 = ( 𝑠 + 1 ) → ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) )
105 fvoveq1 ⊢ ( 𝑘 = ( 𝑠 + 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) = ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) )
106 105 fveq2d ⊢ ( 𝑘 = ( 𝑠 + 1 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) )
107 104 106 oveq12d ⊢ ( 𝑘 = ( 𝑠 + 1 ) → ( ( 𝑘 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) )
108 26 34 6 37 91 95 99 103 107 telgsumfz ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) ) ) ) = ( ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) ) )
109 25 108 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) ) )
110 109 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
111 55 10 mulg1 ⊢ ( ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) → ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( 𝑇 ‘ 𝑀 ) )
112 52 111 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( 𝑇 ‘ 𝑀 ) )
113 112 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) = ( 𝑇 ‘ 𝑀 ) )
114 1cnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 1 ∈ ℂ )
115 114 subidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 1 − 1 ) = 0 )
116 115 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ ( 1 − 1 ) ) = ( 𝑏 ‘ 0 ) )
117 116 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) )
118 113 117 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) )
119 72 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℂ )
120 119 114 pncand ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑠 + 1 ) − 1 ) = 𝑠 )
121 120 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) = ( 𝑏 ‘ 𝑠 ) )
122 121 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) )
123 122 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) = ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) )
124 118 123 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) ) = ( ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) )
125 124 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
126 ringgrp ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
127 31 126 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
128 127 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Grp )
129 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
130 0elfz ⊢ ( 𝑠 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑠 ) )
131 129 130 syl ⊢ ( 𝑠 ∈ ℕ → 0 ∈ ( 0 ... 𝑠 ) )
132 131 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ( 0 ... 𝑠 ) )
133 65 132 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
134 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
135 58 61 133 134 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
136 26 5 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
137 38 53 135 136 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
138 45 47 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
139 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℕ )
140 139 peano2nnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℕ )
141 55 10 mulgnncl ⊢ ( ( ( mulGrp ‘ 𝑌 ) ∈ Mgm ∧ ( 𝑠 + 1 ) ∈ ℕ ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
142 138 140 53 141 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
143 nn0fz0 ⊢ ( 𝑠 ∈ ℕ0 ↔ 𝑠 ∈ ( 0 ... 𝑠 ) )
144 129 143 sylib ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( 0 ... 𝑠 ) )
145 144 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ( 0 ... 𝑠 ) )
146 65 145 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 )
147 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ ( Base ‘ 𝑌 ) )
148 58 61 146 147 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ ( Base ‘ 𝑌 ) )
149 26 5 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) )
150 38 142 148 149 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) )
151 26 11 6 7 grpnpncan0 ⊢ ( ( 𝑌 ∈ Grp ∧ ( ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = 0 )
152 128 137 150 151 syl12anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = 0 )
153 125 152 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( ( 1 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 1 − 1 ) ) ) ) − ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( ( 𝑠 + 1 ) − 1 ) ) ) ) ) ( +g ‘ 𝑌 ) ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = 0 )
154 12 110 153 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑖 ) ) ) ) = 0 )