Metamath Proof Explorer

Theorem chfacfpmmulgsum2

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 chfacfpmmulgsum2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 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 1 2 3 4 5 6 7 8 9 10 11 chfacfpmmulgsum ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
13 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
14 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
15 14 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
16 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
17 15 16 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
18 17 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
19 18 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ Ring )
20 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
21 20 ringmgp ⊢ ( 𝑌 ∈ Ring → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
22 mndmgm ⊢ ( ( mulGrp ‘ 𝑌 ) ∈ Mnd → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
23 21 22 syl ⊢ ( 𝑌 ∈ Ring → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
24 18 23 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
25 24 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( mulGrp ‘ 𝑌 ) ∈ Mgm )
26 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ℕ )
27 26 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ℕ )
28 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
29 14 28 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
30 29 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
31 20 13 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
32 31 10 mulgnncl ⊢ ( ( ( mulGrp ‘ 𝑌 ) ∈ Mgm ∧ 𝑖 ∈ ℕ ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) → ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
33 25 27 30 32 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
34 15 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
35 34 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
36 elmapi ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
37 36 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
38 37 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
39 38 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
40 1nn0 ⊢ 1 ∈ ℕ0
41 40 a1i ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 1 ∈ ℕ0 )
42 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
43 42 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑠 ∈ ℕ0 )
44 nnge1 ⊢ ( 𝑠 ∈ ℕ → 1 ≤ 𝑠 )
45 44 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 1 ≤ 𝑠 )
46 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 𝑠 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 1 ≤ 𝑠 ) )
47 41 43 45 46 syl3anbrc ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 1 ∈ ( 0 ... 𝑠 ) )
48 simpr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑖 ∈ ( 1 ... 𝑠 ) )
49 fz0fzdiffz0 ⊢ ( ( 1 ∈ ( 0 ... 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
50 47 48 49 syl2anc ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
51 50 ex ⊢ ( 𝑠 ∈ ℕ → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
52 51 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) ) )
53 52 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ... 𝑠 ) )
54 39 53 ffvelrnd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 )
55 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ) )
56 35 54 55 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ) )
57 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
58 56 57 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
59 34 16 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
60 59 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → 𝑌 ∈ Ring )
61 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
62 14 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
63 62 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
64 42 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ℕ0 )
65 61 63 64 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
66 65 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
67 simpr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
68 67 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) )
69 fz1ssfz0 ⊢ ( 1 ... 𝑠 ) ⊆ ( 0 ... 𝑠 )
70 69 sseli ⊢ ( 𝑖 ∈ ( 1 ... 𝑠 ) → 𝑖 ∈ ( 0 ... 𝑠 ) )
71 68 70 anim12i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) )
72 1 2 3 4 8 m2pmfzmap ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
73 66 71 72 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) )
74 13 5 ringcl ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
75 60 30 73 74 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑌 ) )
76 13 5 6 19 33 58 75 ringsubdi ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
77 13 5 ringass ⊢ ( ( 𝑌 ∈ Ring ∧ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑌 ) ) ) → ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
78 60 33 30 73 77 syl13anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
79 78 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
80 29 31 eleqtrdi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) )
81 80 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) )
82 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
83 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( mulGrp ‘ 𝑌 ) )
84 82 10 83 mulgnnp1 ⊢ ( ( 𝑖 ∈ ℕ ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ) → ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) ( +g ‘ ( mulGrp ‘ 𝑌 ) ) ( 𝑇 ‘ 𝑀 ) ) )
85 26 81 84 syl2anr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) ( +g ‘ ( mulGrp ‘ 𝑌 ) ) ( 𝑇 ‘ 𝑀 ) ) )
86 20 5 mgpplusg ⊢ × = ( +g ‘ ( mulGrp ‘ 𝑌 ) )
87 86 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ×
88 87 a1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = × )
89 88 oveqd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) ( +g ‘ ( mulGrp ‘ 𝑌 ) ) ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) )
90 85 89 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) )
91 90 eqcomd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) = ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) )
92 91 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
93 79 92 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
94 93 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
95 76 94 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑠 ) ) → ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
96 95 mpteq2dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
97 96 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
98 97 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
99 12 98 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑌 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑖 ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( ( 𝑖 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − ( ( ( 𝑖 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )