Metamath Proof Explorer

Theorem chfacfisfcpmat

Description: The "characteristic factor function" is a function from the nonnegative integers to constant polynomial matrices. (Contributed by AV, 19-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 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
chfacfisfcpmat.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
Assertion chfacfisfcpmat ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ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 chfacfisfcpmat.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
11 10 3 4 cpmatsubgpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝑌 ) )
12 11 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑆 ∈ ( SubGrp ‘ 𝑌 ) )
13 12 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑌 ) )
14 subgsubm ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑌 ) → 𝑆 ∈ ( SubMnd ‘ 𝑌 ) )
15 7 subm0cl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑌 ) → 0 ∈ 𝑆 )
16 12 14 15 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 0 ∈ 𝑆 )
17 16 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 0 ∈ 𝑆 )
18 10 3 4 cpmatsrgpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝑌 ) )
19 18 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑆 ∈ ( SubRing ‘ 𝑌 ) )
20 19 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑆 ∈ ( SubRing ‘ 𝑌 ) )
21 10 8 1 2 m2cpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝑆 )
22 21 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝑆 )
23 3simpa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
24 elmapi ⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
25 24 adantl ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
26 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
27 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
28 26 27 eleqtrdi ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( ℤ≥ ‘ 0 ) )
29 eluzfz1 ⊢ ( 𝑠 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑠 ) )
30 28 29 syl ⊢ ( 𝑠 ∈ ℕ → 0 ∈ ( 0 ... 𝑠 ) )
31 30 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 0 ∈ ( 0 ... 𝑠 ) )
32 25 31 ffvelrnd ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑏 ‘ 0 ) ∈ 𝐵 )
33 23 32 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
34 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
35 33 34 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) )
36 10 8 1 2 m2cpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 0 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ 𝑆 )
37 35 36 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ 𝑆 )
38 5 subrgmcl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ 𝑆 ∧ ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ∈ 𝑆 ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ 𝑆 )
39 20 22 37 38 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ 𝑆 )
40 6 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝑌 ) ∧ 0 ∈ 𝑆 ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ∈ 𝑆 ) → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ 𝑆 )
41 13 17 39 40 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ 𝑆 )
42 41 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ 𝑆 )
43 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑁 ∈ Fin )
44 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑅 ∈ Ring )
45 25 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
46 eluzfz2 ⊢ ( 𝑠 ∈ ( ℤ≥ ‘ 0 ) → 𝑠 ∈ ( 0 ... 𝑠 ) )
47 28 46 syl ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ( 0 ... 𝑠 ) )
48 47 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑠 ∈ ( 0 ... 𝑠 ) )
49 45 48 ffvelrnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 )
50 10 8 1 2 m2cpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 𝑠 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ 𝑆 )
51 43 44 49 50 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ 𝑆 )
52 51 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ 𝑆 )
53 52 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 = ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ 𝑆 )
54 17 ad4antr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ( 𝑠 + 1 ) < 𝑛 ) → 0 ∈ 𝑆 )
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 12 ad4antr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑌 ) )
75 23 ad4antr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
76 25 ad4antlr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
77 neqne ⊢ ( ¬ 𝑛 = 0 → 𝑛 ≠ 0 )
78 77 anim2i ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0 ) → ( 𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0 ) )
79 elnnne0 ⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0 ) )
80 78 79 sylibr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ )
81 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
82 80 81 syl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0 ) → ( 𝑛 − 1 ) ∈ ℕ0 )
83 82 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
84 26 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
85 84 ad4antlr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑠 ∈ ℕ0 )
86 63 simprbda ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ≤ ( 𝑠 + 1 ) )
87 56 adantr ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ℝ )
88 1red ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 1 ∈ ℝ )
89 nnre ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℝ )
90 89 ad2antrr ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑠 ∈ ℝ )
91 87 88 90 lesubaddd ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑛 − 1 ) ≤ 𝑠 ↔ 𝑛 ≤ ( 𝑠 + 1 ) ) )
92 86 91 mpbird ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ≤ 𝑠 )
93 92 exp31 ⊢ ( 𝑠 ∈ ℕ → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) ) )
94 93 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) ) )
95 94 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) )
96 95 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑛 < ( 𝑠 + 1 ) → ( 𝑛 − 1 ) ≤ 𝑠 ) )
97 96 imp ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ≤ 𝑠 )
98 elfz2nn0 ⊢ ( ( 𝑛 − 1 ) ∈ ( 0 ... 𝑠 ) ↔ ( ( 𝑛 − 1 ) ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ ( 𝑛 − 1 ) ≤ 𝑠 ) )
99 83 85 97 98 syl3anbrc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ... 𝑠 ) )
100 76 99 ffvelrnd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 )
101 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) )
102 75 100 101 sylanbrc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) )
103 10 8 1 2 m2cpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ∈ 𝑆 )
104 102 103 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ∈ 𝑆 )
105 20 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑌 ) )
106 22 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝑆 )
107 23 84 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ ℕ0 ) )
108 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑠 ∈ ℕ0 ) )
109 107 108 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
110 109 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0 ) )
111 110 simp1d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑁 ∈ Fin )
112 110 simp2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑅 ∈ Ring )
113 45 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
114 simplr ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ℕ0 )
115 26 ad2antrr ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑠 ∈ ℕ0 )
116 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
117 nnz ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
118 zleltp1 ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑛 ≤ 𝑠 ↔ 𝑛 < ( 𝑠 + 1 ) ) )
119 116 117 118 syl2anr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ 𝑠 ↔ 𝑛 < ( 𝑠 + 1 ) ) )
120 119 biimpar ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ≤ 𝑠 )
121 elfz2nn0 ⊢ ( 𝑛 ∈ ( 0 ... 𝑠 ) ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑛 ≤ 𝑠 ) )
122 114 115 120 121 syl3anbrc ⊢ ( ( ( 𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ( 0 ... 𝑠 ) )
123 122 exp31 ⊢ ( 𝑠 ∈ ℕ → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → 𝑛 ∈ ( 0 ... 𝑠 ) ) ) )
124 123 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 → ( 𝑛 < ( 𝑠 + 1 ) → 𝑛 ∈ ( 0 ... 𝑠 ) ) ) )
125 124 imp31 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → 𝑛 ∈ ( 0 ... 𝑠 ) )
126 113 125 ffvelrnd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
127 10 8 1 2 m2cpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ∈ 𝑆 )
128 111 112 126 127 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ∈ 𝑆 )
129 5 subrgmcl ⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ 𝑆 ∧ ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ∈ 𝑆 ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ 𝑆 )
130 105 106 128 129 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ 𝑆 )
131 130 adantlr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ 𝑆 )
132 6 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝑌 ) ∧ ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ∈ 𝑆 ∧ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ 𝑆 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ∈ 𝑆 )
133 74 104 131 132 syl3anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ 𝑛 < ( 𝑠 + 1 ) ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ∈ 𝑆 )
134 133 ex ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( 𝑛 < ( 𝑠 + 1 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ∈ 𝑆 ) )
135 73 134 syld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ( ( ¬ 𝑛 = ( 𝑠 + 1 ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ∈ 𝑆 ) )
136 135 impl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) ∧ ¬ ( 𝑠 + 1 ) < 𝑛 ) → ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ∈ 𝑆 )
137 54 136 ifclda ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) ∧ ¬ 𝑛 = ( 𝑠 + 1 ) ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ∈ 𝑆 )
138 53 137 ifclda ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ∈ 𝑆 )
139 42 138 ifclda ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) ∈ 𝑆 )
140 139 9 fmptd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ 𝑆 )