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 ‘ 𝑌 ) )