Metamath Proof Explorer

Theorem chfacfscmul0

Description: A scaled value of the "characteristic factor function" is zero almost always. (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 ‘ 𝑃 ) )
Assertion chfacfscmul0 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 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 eluz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ↔ ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) )
14 simpll ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 𝐾 ∈ ℤ )
15 nngt0 ⊢ ( 𝑠 ∈ ℕ → 0 < 𝑠 )
16 nnre ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℝ )
17 16 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 ∈ ℝ )
18 2rp ⊢ 2 ∈ ℝ+
19 18 a1i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 2 ∈ ℝ+ )
20 17 19 ltaddrpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 < ( 𝑠 + 2 ) )
21 0red ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 0 ∈ ℝ )
22 2re ⊢ 2 ∈ ℝ
23 22 a1i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 2 ∈ ℝ )
24 17 23 readdcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑠 + 2 ) ∈ ℝ )
25 lttr ⊢ ( ( 0 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ ( 𝑠 + 2 ) ∈ ℝ ) → ( ( 0 < 𝑠 ∧ 𝑠 < ( 𝑠 + 2 ) ) → 0 < ( 𝑠 + 2 ) ) )
26 21 17 24 25 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 0 < 𝑠 ∧ 𝑠 < ( 𝑠 + 2 ) ) → 0 < ( 𝑠 + 2 ) ) )
27 20 26 mpan2d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 0 < 𝑠 → 0 < ( 𝑠 + 2 ) ) )
28 27 ex ⊢ ( 𝐾 ∈ ℤ → ( 𝑠 ∈ ℕ → ( 0 < 𝑠 → 0 < ( 𝑠 + 2 ) ) ) )
29 28 com13 ⊢ ( 0 < 𝑠 → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℤ → 0 < ( 𝑠 + 2 ) ) ) )
30 15 29 mpcom ⊢ ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℤ → 0 < ( 𝑠 + 2 ) ) )
31 30 impcom ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 0 < ( 𝑠 + 2 ) )
32 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
33 32 adantr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝐾 ∈ ℝ )
34 ltleletr ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑠 + 2 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 0 < ( 𝑠 + 2 ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 ) )
35 21 24 33 34 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 0 < ( 𝑠 + 2 ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 ) )
36 31 35 mpand ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 → 0 ≤ 𝐾 ) )
37 36 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 )
38 elnn0z ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
39 14 37 38 sylanbrc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 𝐾 ∈ ℕ0 )
40 nncn ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
41 add1p1 ⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
42 40 41 syl ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
43 42 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
44 43 eqcomd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑠 + 2 ) = ( ( 𝑠 + 1 ) + 1 ) )
45 44 breq1d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ) )
46 nnz ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
47 46 peano2zd ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℤ )
48 47 anim2i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝐾 ∈ ℤ ∧ ( 𝑠 + 1 ) ∈ ℤ ) )
49 48 ancomd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
50 zltp1le ⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑠 + 1 ) < 𝐾 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ) )
51 50 bicomd ⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
52 49 51 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
53 45 52 bitrd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
54 53 biimpa ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
55 39 54 jca ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) )
56 55 ex ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
57 56 impancom ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
58 57 3adant1 ⊢ ( ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
59 58 com12 ⊢ ( 𝑠 ∈ ℕ → ( ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
60 13 59 syl5bi ⊢ ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
61 60 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
62 61 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
63 0red ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 ∈ ℝ )
64 peano2re ⊢ ( 𝑠 ∈ ℝ → ( 𝑠 + 1 ) ∈ ℝ )
65 16 64 syl ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℝ )
66 65 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
67 66 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
68 67 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑠 + 1 ) ∈ ℝ )
69 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
70 69 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ∈ ℝ )
71 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
72 71 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
73 72 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑠 ∈ ℕ0 )
74 nn0p1gt0 ⊢ ( 𝑠 ∈ ℕ0 → 0 < ( 𝑠 + 1 ) )
75 73 74 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 0 < ( 𝑠 + 1 ) )
76 75 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 < ( 𝑠 + 1 ) )
77 simpr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
78 63 68 70 76 77 lttrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 < 𝐾 )
79 78 gt0ne0d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ 0 )
80 79 neneqd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ¬ 𝐾 = 0 )
81 80 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝐾 = 0 )
82 eqeq1 ⊢ ( 𝑛 = 𝐾 → ( 𝑛 = 0 ↔ 𝐾 = 0 ) )
83 82 notbid ⊢ ( 𝑛 = 𝐾 → ( ¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0 ) )
84 83 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0 ) )
85 81 84 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝑛 = 0 )
86 85 iffalsed ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) )
87 66 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑠 + 1 ) ∈ ℝ )
88 ltne ⊢ ( ( ( 𝑠 + 1 ) ∈ ℝ ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ ( 𝑠 + 1 ) )
89 87 88 sylan ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ ( 𝑠 + 1 ) )
90 89 neneqd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ¬ 𝐾 = ( 𝑠 + 1 ) )
91 90 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝐾 = ( 𝑠 + 1 ) )
92 eqeq1 ⊢ ( 𝑛 = 𝐾 → ( 𝑛 = ( 𝑠 + 1 ) ↔ 𝐾 = ( 𝑠 + 1 ) ) )
93 92 notbid ⊢ ( 𝑛 = 𝐾 → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝐾 = ( 𝑠 + 1 ) ) )
94 93 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝐾 = ( 𝑠 + 1 ) ) )
95 91 94 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝑛 = ( 𝑠 + 1 ) )
96 95 iffalsed ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) )
97 simplr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
98 breq2 ⊢ ( 𝑛 = 𝐾 → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
99 98 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
100 97 99 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( 𝑠 + 1 ) < 𝑛 )
101 100 iftrued ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = 0 )
102 86 96 101 3eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = 0 )
103 simplr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ∈ ℕ0 )
104 7 fvexi ⊢ 0 ∈ V
105 104 a1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 ∈ V )
106 9 102 103 105 fvmptd2 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝐺 ‘ 𝐾 ) = 0 )
107 106 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = ( ( 𝐾 ↑ 𝑋 ) · 0 ) )
108 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
109 3 4 pmatlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
110 108 109 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
111 110 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ LMod )
112 111 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑌 ∈ LMod )
113 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
114 108 113 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
115 114 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
116 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
117 116 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
118 115 117 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
119 118 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
120 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
121 108 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
122 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
123 10 3 122 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
124 121 123 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
125 124 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
126 116 122 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
127 126 12 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝐾 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
128 119 120 125 127 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
129 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
130 129 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
131 130 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
132 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
133 131 132 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
134 133 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
135 134 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
136 135 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
137 136 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ↔ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) )
138 128 137 mpbird ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
139 112 138 jca ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) )
140 139 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) )
141 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
142 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
143 141 11 142 7 lmodvs0 ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) → ( ( 𝐾 ↑ 𝑋 ) · 0 ) = 0 )
144 140 143 syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · 0 ) = 0 )
145 107 144 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 )
146 145 expl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 ) )
147 62 146 syld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 ) )
148 147 3impia ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) = 0 )