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 ffvelrnd ( ( ( 𝑁 ∈ 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 ffvelrnd ( ( ( 𝑁 ∈ 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 ) ) ) ) ) )