Metamath Proof Explorer

Theorem chfacfpmmul0

Description: The value of the "characteristic factor function" multiplied with a constant polynomial matrix is zero almost always. (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses cayhamlem1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cayhamlem1.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cayhamlem1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cayhamlem1.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
cayhamlem1.r ⊢ × = ( .r ‘ 𝑌 )
cayhamlem1.s ⊢ − = ( -g ‘ 𝑌 )
cayhamlem1.0 ⊢ 0 = ( 0g ‘ 𝑌 )
cayhamlem1.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
cayhamlem1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
cayhamlem1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
Assertion chfacfpmmul0 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 cayhamlem1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 cayhamlem1.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 cayhamlem1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cayhamlem1.y ⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5 cayhamlem1.r ⊢ × = ( .r ‘ 𝑌 )
6 cayhamlem1.s ⊢ − = ( -g ‘ 𝑌 )
7 cayhamlem1.0 ⊢ 0 = ( 0g ‘ 𝑌 )
8 cayhamlem1.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9 cayhamlem1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
10 cayhamlem1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
11 eluz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ↔ ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) )
12 simpll ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 𝐾 ∈ ℤ )
13 nngt0 ⊢ ( 𝑠 ∈ ℕ → 0 < 𝑠 )
14 nnre ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℝ )
15 14 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 ∈ ℝ )
16 2rp ⊢ 2 ∈ ℝ+
17 16 a1i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 2 ∈ ℝ+ )
18 15 17 ltaddrpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 < ( 𝑠 + 2 ) )
19 0red ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 0 ∈ ℝ )
20 2re ⊢ 2 ∈ ℝ
21 20 a1i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 2 ∈ ℝ )
22 15 21 readdcld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑠 + 2 ) ∈ ℝ )
23 lttr ⊢ ( ( 0 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ ( 𝑠 + 2 ) ∈ ℝ ) → ( ( 0 < 𝑠 ∧ 𝑠 < ( 𝑠 + 2 ) ) → 0 < ( 𝑠 + 2 ) ) )
24 19 15 22 23 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 0 < 𝑠 ∧ 𝑠 < ( 𝑠 + 2 ) ) → 0 < ( 𝑠 + 2 ) ) )
25 18 24 mpan2d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 0 < 𝑠 → 0 < ( 𝑠 + 2 ) ) )
26 25 ex ⊢ ( 𝐾 ∈ ℤ → ( 𝑠 ∈ ℕ → ( 0 < 𝑠 → 0 < ( 𝑠 + 2 ) ) ) )
27 26 com13 ⊢ ( 0 < 𝑠 → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℤ → 0 < ( 𝑠 + 2 ) ) ) )
28 13 27 mpcom ⊢ ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℤ → 0 < ( 𝑠 + 2 ) ) )
29 28 impcom ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 0 < ( 𝑠 + 2 ) )
30 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
31 30 adantr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝐾 ∈ ℝ )
32 ltleletr ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑠 + 2 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 0 < ( 𝑠 + 2 ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 ) )
33 19 22 31 32 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 0 < ( 𝑠 + 2 ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 ) )
34 29 33 mpand ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 → 0 ≤ 𝐾 ) )
35 34 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 0 ≤ 𝐾 )
36 elnn0z ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
37 12 35 36 sylanbrc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → 𝐾 ∈ ℕ0 )
38 nncn ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℂ )
39 add1p1 ⊢ ( 𝑠 ∈ ℂ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
40 38 39 syl ⊢ ( 𝑠 ∈ ℕ → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
41 40 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) + 1 ) = ( 𝑠 + 2 ) )
42 41 eqcomd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑠 + 2 ) = ( ( 𝑠 + 1 ) + 1 ) )
43 42 breq1d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ) )
44 nnz ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
45 44 peano2zd ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℤ )
46 45 anim2i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝐾 ∈ ℤ ∧ ( 𝑠 + 1 ) ∈ ℤ ) )
47 46 ancomd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
48 zltp1le ⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑠 + 1 ) < 𝐾 ↔ ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ) )
49 48 bicomd ⊢ ( ( ( 𝑠 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
50 47 49 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( ( 𝑠 + 1 ) + 1 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
51 43 50 bitrd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
52 51 biimpa ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
53 37 52 jca ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) )
54 53 ex ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑠 + 2 ) ≤ 𝐾 → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
55 54 impancom ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
56 55 3adant1 ⊢ ( ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
57 56 com12 ⊢ ( 𝑠 ∈ ℕ → ( ( ( 𝑠 + 2 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑠 + 2 ) ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
58 11 57 biimtrid ⊢ ( 𝑠 ∈ ℕ → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
59 58 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
60 59 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) ) )
61 0red ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 ∈ ℝ )
62 peano2re ⊢ ( 𝑠 ∈ ℝ → ( 𝑠 + 1 ) ∈ ℝ )
63 14 62 syl ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℝ )
64 63 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
65 64 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
66 65 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑠 + 1 ) ∈ ℝ )
67 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
68 67 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ∈ ℝ )
69 nnnn0 ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 )
70 69 adantr ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 )
71 70 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑠 ∈ ℕ0 )
72 nn0p1gt0 ⊢ ( 𝑠 ∈ ℕ0 → 0 < ( 𝑠 + 1 ) )
73 71 72 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 0 < ( 𝑠 + 1 ) )
74 73 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 < ( 𝑠 + 1 ) )
75 simpr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
76 61 66 68 74 75 lttrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 < 𝐾 )
77 76 gt0ne0d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ 0 )
78 77 neneqd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ¬ 𝐾 = 0 )
79 78 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝐾 = 0 )
80 eqeq1 ⊢ ( 𝑛 = 𝐾 → ( 𝑛 = 0 ↔ 𝐾 = 0 ) )
81 80 notbid ⊢ ( 𝑛 = 𝐾 → ( ¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0 ) )
82 81 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ¬ 𝑛 = 0 ↔ ¬ 𝐾 = 0 ) )
83 79 82 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝑛 = 0 )
84 83 iffalsed ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) )
85 64 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑠 + 1 ) ∈ ℝ )
86 ltne ⊢ ( ( ( 𝑠 + 1 ) ∈ ℝ ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ ( 𝑠 + 1 ) )
87 85 86 sylan ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ≠ ( 𝑠 + 1 ) )
88 87 neneqd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ¬ 𝐾 = ( 𝑠 + 1 ) )
89 88 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝐾 = ( 𝑠 + 1 ) )
90 eqeq1 ⊢ ( 𝑛 = 𝐾 → ( 𝑛 = ( 𝑠 + 1 ) ↔ 𝐾 = ( 𝑠 + 1 ) ) )
91 90 notbid ⊢ ( 𝑛 = 𝐾 → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝐾 = ( 𝑠 + 1 ) ) )
92 91 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝐾 = ( 𝑠 + 1 ) ) )
93 89 92 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ¬ 𝑛 = ( 𝑠 + 1 ) )
94 93 iffalsed ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) )
95 simplr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( 𝑠 + 1 ) < 𝐾 )
96 breq2 ⊢ ( 𝑛 = 𝐾 → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
97 96 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝐾 ) )
98 95 97 mpbird ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → ( 𝑠 + 1 ) < 𝑛 )
99 98 iftrued ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = 0 )
100 84 94 99 3eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) ∧ 𝑛 = 𝐾 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = 0 )
101 simplr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝐾 ∈ ℕ0 )
102 7 fvexi ⊢ 0 ∈ V
103 102 a1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 0 ∈ V )
104 9 100 101 103 fvmptd2 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝐺 ‘ 𝐾 ) = 0 )
105 104 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) = ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × 0 ) )
106 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
107 3 4 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
108 106 107 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
109 108 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
110 109 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑌 ∈ Ring )
111 110 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → 𝑌 ∈ Ring )
112 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
113 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
114 112 113 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
115 112 ringmgp ⊢ ( 𝑌 ∈ Ring → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
116 109 115 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
117 116 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( mulGrp ‘ 𝑌 ) ∈ Mnd )
118 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
119 8 1 2 3 4 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
120 106 119 syl3an2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
121 120 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
122 114 10 117 118 121 mulgnn0cld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
123 122 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
124 113 5 7 ringrz ⊢ ( ( 𝑌 ∈ Ring ∧ ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × 0 ) = 0 )
125 111 123 124 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × 0 ) = 0 )
126 105 125 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) = 0 )
127 126 expl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑠 + 1 ) < 𝐾 ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) = 0 ) )
128 60 127 syld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) = 0 ) )
129 128 3impia ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑠 + 2 ) ) ) → ( ( 𝐾 ↑ ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝐾 ) ) = 0 )