Metamath Proof Explorer


Theorem chfacfisf

Description: The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-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 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ) )
Assertion chfacfisf ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )

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 3 4 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
11 10 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑌 ∈ Ring )
12 ringgrp ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
13 11 12 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑌 ∈ Grp )
14 13 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Grp )
15 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 15 7 ring0cl ( 𝑌 ∈ Ring → 0 ∈ ( Base ‘ 𝑌 ) )
17 11 16 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 0 ∈ ( Base ‘ 𝑌 ) )
18 17 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ ( Base ‘ 𝑌 ) )
19 11 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
20 8 1 2 3 4 mat2pmatbas ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) )
21 20 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) )
22 3simpa ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23 elmapi ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
24 23 adantl ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
25 nnnn0 ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
26 nn0uz 0 = ( ℤ ‘ 0 )
27 25 26 eleqtrdi ( 𝑠 ∈ ℕ → 𝑠 ∈ ( ℤ ‘ 0 ) )
28 eluzfz1 ( 𝑠 ∈ ( ℤ ‘ 0 ) → 0 ∈ ( 0 ... 𝑠 ) )
29 27 28 syl ( 𝑠 ∈ ℕ → 0 ∈ ( 0 ... 𝑠 ) )
30 29 adantr ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 0 ∈ ( 0 ... 𝑠 ) )
31 24 30 ffvelrnd ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
32 22 31 anim12i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
33 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
34 32 33 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
35 8 1 2 3 4 mat2pmatbas ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
36 34 35 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) )
37 15 5 ringcl ( ( 𝑌 ∈ Ring ∧ ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
38 19 21 36 37 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) )
39 15 6 grpsubcl ( ( 𝑌 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
40 14 18 38 39 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
41 40 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
42 25 adantr ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
43 22 42 anim12i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ ℕ0 ) )
44 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ ℕ0 ) )
45 43 44 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
46 eluzfz2 ( 𝑠 ∈ ( ℤ ‘ 0 ) → 𝑠 ∈ ( 0 ... 𝑠 ) )
47 27 46 syl ( 𝑠 ∈ ℕ → 𝑠 ∈ ( 0 ... 𝑠 ) )
48 47 anim1ci ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑠 ∈ ( 0 ... 𝑠 ) ) )
49 48 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑠 ∈ ( 0 ... 𝑠 ) ) )
50 1 2 3 4 8 m2pmfzmap ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑠 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏𝑠 ) ) ∈ ( Base ‘ 𝑌 ) )
51 45 49 50 syl2anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏𝑠 ) ) ∈ ( Base ‘ 𝑌 ) )
52 51 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑏𝑠 ) ) ∈ ( Base ‘ 𝑌 ) )
53 52 ad2antrr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 = ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏𝑠 ) ) ∈ ( Base ‘ 𝑌 ) )
54 18 ad4antr ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ( 𝑠 + 1 ) < 𝑛 ) → 0 ∈ ( Base ‘ 𝑌 ) )
55 nn0re ( 𝑛 ∈ ℕ0𝑛 ∈ ℝ )
56 55 adantl ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℝ )
57 peano2nn ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℕ )
58 57 nnred ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℝ )
59 58 adantr ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑠 + 1 ) ∈ ℝ )
60 56 59 lenltd ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ ( 𝑠 + 1 ) ↔ ¬ ( 𝑠 + 1 ) < 𝑛 ) )
61 nesym ( ( 𝑠 + 1 ) ≠ 𝑛 ↔ ¬ 𝑛 = ( 𝑠 + 1 ) )
62 ltlen ( ( 𝑛 ∈ ℝ ∧ ( 𝑠 + 1 ) ∈ ℝ ) → ( 𝑛 < ( 𝑠 + 1 ) ↔ ( 𝑛 ≤ ( 𝑠 + 1 ) ∧ ( 𝑠 + 1 ) ≠ 𝑛 ) ) )
63 55 58 62 syl2anr ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 < ( 𝑠 + 1 ) ↔ ( 𝑛 ≤ ( 𝑠 + 1 ) ∧ ( 𝑠 + 1 ) ≠ 𝑛 ) ) )
64 63 biimprd ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( 𝑠 + 1 ) ∧ ( 𝑠 + 1 ) ≠ 𝑛 ) → 𝑛 < ( 𝑠 + 1 ) ) )
65 64 expcomd ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 + 1 ) ≠ 𝑛 → ( 𝑛 ≤ ( 𝑠 + 1 ) → 𝑛 < ( 𝑠 + 1 ) ) ) )
66 61 65 syl5bir ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑛 = ( 𝑠 + 1 ) → ( 𝑛 ≤ ( 𝑠 + 1 ) → 𝑛 < ( 𝑠 + 1 ) ) ) )
67 66 com23 ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ ( 𝑠 + 1 ) → ( ¬ 𝑛 = ( 𝑠 + 1 ) → 𝑛 < ( 𝑠 + 1 ) ) ) )
68 60 67 sylbird ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( ¬ ( 𝑠 + 1 ) < 𝑛 → ( ¬ 𝑛 = ( 𝑠 + 1 ) → 𝑛 < ( 𝑠 + 1 ) ) ) )
69 68 impcomd ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → 𝑛 < ( 𝑠 + 1 ) ) )
70 69 ex ( 𝑠 ∈ ℕ → ( 𝑛 ∈ ℕ0 → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → 𝑛 < ( 𝑠 + 1 ) ) ) )
71 70 ad2antrl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → 𝑛 < ( 𝑠 + 1 ) ) ) )
72 71 imp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → 𝑛 < ( 𝑠 + 1 ) ) )
73 72 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → 𝑛 < ( 𝑠 + 1 ) ) )
74 10 12 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Grp )
75 74 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑌 ∈ Grp )
76 75 ad4antr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑌 ∈ Grp )
77 22 ad4antr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
78 24 ad4antlr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
79 neqne ( ¬ 𝑛 = 0 → 𝑛 ≠ 0 )
80 79 anim2i ( ( 𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0 ) → ( 𝑛 ∈ ℕ0𝑛 ≠ 0 ) )
81 elnnne0 ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℕ0𝑛 ≠ 0 ) )
82 80 81 sylibr ( ( 𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ )
83 nnm1nn0 ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
84 82 83 syl ( ( 𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0 ) → ( 𝑛 − 1 ) ∈ ℕ0 )
85 84 ad4ant23 ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
86 42 ad4antlr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑠 ∈ ℕ0 )
87 63 simprbda ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ≤ ( 𝑠 + 1 ) )
88 56 adantr ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ℝ )
89 1red ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 1 ∈ ℝ )
90 nnre ( 𝑠 ∈ ℕ → 𝑠 ∈ ℝ )
91 90 ad2antrr ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑠 ∈ ℝ )
92 88 89 91 lesubaddd ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑛 − 1 ) ≤ 𝑠𝑛 ≤ ( 𝑠 + 1 ) ) )
93 87 92 mpbird ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ≤ 𝑠 )
94 93 exp31 ( 𝑠 ∈ ℕ → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) ) )
95 94 ad2antrl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) ) )
96 95 imp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) )
97 96 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) )
98 97 imp ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ≤ 𝑠 )
99 elfz2nn0 ( ( 𝑛 − 1 ) ∈ ( 0 ... 𝑠 ) ↔ ( ( 𝑛 − 1 ) ∈ ℕ0𝑠 ∈ ℕ0 ∧ ( 𝑛 − 1 ) ≤ 𝑠 ) )
100 85 86 98 99 syl3anbrc ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ... 𝑠 ) )
101 78 100 ffvelrnd ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 )
102 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) )
103 77 101 102 sylanbrc ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) )
104 8 1 2 3 4 mat2pmatbas ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
105 103 104 syl ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) )
106 19 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑌 ∈ Ring )
107 21 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) )
108 45 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
109 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) )
110 109 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) )
111 simplr ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ℕ0 )
112 25 ad2antrr ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑠 ∈ ℕ0 )
113 nn0z ( 𝑛 ∈ ℕ0𝑛 ∈ ℤ )
114 nnz ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
115 zleltp1 ( ( 𝑛 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑛𝑠𝑛 < ( 𝑠 + 1 ) ) )
116 113 114 115 syl2anr ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛𝑠𝑛 < ( 𝑠 + 1 ) ) )
117 116 biimpar ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛𝑠 )
118 elfz2nn0 ( 𝑛 ∈ ( 0 ... 𝑠 ) ↔ ( 𝑛 ∈ ℕ0𝑠 ∈ ℕ0𝑛𝑠 ) )
119 111 112 117 118 syl3anbrc ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ( 0 ... 𝑠 ) )
120 119 exp31 ( 𝑠 ∈ ℕ → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → 𝑛 ∈ ( 0 ... 𝑠 ) ) ) )
121 120 ad2antrl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → 𝑛 ∈ ( 0 ... 𝑠 ) ) ) )
122 121 imp31 ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ( 0 ... 𝑠 ) )
123 1 2 3 4 8 m2pmfzmap ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ∧ ( 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ∧ 𝑛 ∈ ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝑏𝑛 ) ) ∈ ( Base ‘ 𝑌 ) )
124 108 110 122 123 syl12anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏𝑛 ) ) ∈ ( Base ‘ 𝑌 ) )
125 15 5 ringcl ( ( 𝑌 ∈ Ring ∧ ( 𝑇𝑀 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏𝑛 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) )
126 106 107 124 125 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) )
127 126 adantlr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) )
128 15 6 grpsubcl ( ( 𝑌 ∈ Grp ∧ ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
129 76 105 127 128 syl3anc ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
130 129 ex ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑛 < ( 𝑠 + 1 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) )
131 73 130 syld ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ∈ ( Base ‘ 𝑌 ) ) )
132 131 impl ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
133 54 132 ifclda ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
134 53 133 ifclda ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
135 41 134 ifclda ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑛 = 0 , ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
136 135 9 fmptd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )