| 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 |
|
fvexd |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 0g ‘ 𝑌 ) ∈ V ) |
| 11 |
|
ovex |
⊢ ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ∈ V |
| 12 |
|
fvex |
⊢ ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ∈ V |
| 13 |
7
|
fvexi |
⊢ 0 ∈ V |
| 14 |
|
ovex |
⊢ ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ∈ V |
| 15 |
13 14
|
ifex |
⊢ if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ∈ V |
| 16 |
12 15
|
ifex |
⊢ if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ∈ V |
| 17 |
11 16
|
ifex |
⊢ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) ∈ V |
| 18 |
17
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) ∈ V ) |
| 19 |
|
nnnn0 |
⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℕ0 ) |
| 20 |
|
peano2nn0 |
⊢ ( 𝑠 ∈ ℕ0 → ( 𝑠 + 1 ) ∈ ℕ0 ) |
| 21 |
19 20
|
syl |
⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℕ0 ) |
| 22 |
21
|
ad2antrl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑠 + 1 ) ∈ ℕ0 ) |
| 23 |
|
simplr |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ∈ ℕ0 ) |
| 24 |
|
0red |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 0 ∈ ℝ ) |
| 25 |
|
nnre |
⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℝ ) |
| 26 |
|
peano2re |
⊢ ( 𝑠 ∈ ℝ → ( 𝑠 + 1 ) ∈ ℝ ) |
| 27 |
25 26
|
syl |
⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℝ ) |
| 28 |
27
|
adantr |
⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑠 + 1 ) ∈ ℝ ) |
| 29 |
28
|
ad3antlr |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( 𝑠 + 1 ) ∈ ℝ ) |
| 30 |
|
nn0re |
⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ ) |
| 31 |
30
|
ad2antlr |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ∈ ℝ ) |
| 32 |
19
|
adantr |
⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ0 ) |
| 33 |
32
|
ad2antlr |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑠 ∈ ℕ0 ) |
| 34 |
|
nn0p1gt0 |
⊢ ( 𝑠 ∈ ℕ0 → 0 < ( 𝑠 + 1 ) ) |
| 35 |
33 34
|
syl |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 0 < ( 𝑠 + 1 ) ) |
| 36 |
35
|
adantr |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 0 < ( 𝑠 + 1 ) ) |
| 37 |
|
simpr |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ( 𝑠 + 1 ) < 𝑘 ) |
| 38 |
24 29 31 36 37
|
lttrd |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 0 < 𝑘 ) |
| 39 |
38
|
gt0ne0d |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ≠ 0 ) |
| 40 |
39
|
neneqd |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ¬ 𝑘 = 0 ) |
| 41 |
40
|
adantr |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ¬ 𝑘 = 0 ) |
| 42 |
|
eqeq1 |
⊢ ( 𝑛 = 𝑘 → ( 𝑛 = 0 ↔ 𝑘 = 0 ) ) |
| 43 |
42
|
notbid |
⊢ ( 𝑛 = 𝑘 → ( ¬ 𝑛 = 0 ↔ ¬ 𝑘 = 0 ) ) |
| 44 |
43
|
adantl |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ( ¬ 𝑛 = 0 ↔ ¬ 𝑘 = 0 ) ) |
| 45 |
41 44
|
mpbird |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ¬ 𝑛 = 0 ) |
| 46 |
45
|
iffalsed |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) |
| 47 |
28
|
ad2antlr |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑠 + 1 ) ∈ ℝ ) |
| 48 |
|
ltne |
⊢ ( ( ( 𝑠 + 1 ) ∈ ℝ ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ≠ ( 𝑠 + 1 ) ) |
| 49 |
47 48
|
sylan |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → 𝑘 ≠ ( 𝑠 + 1 ) ) |
| 50 |
49
|
neneqd |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ¬ 𝑘 = ( 𝑠 + 1 ) ) |
| 51 |
50
|
adantr |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ¬ 𝑘 = ( 𝑠 + 1 ) ) |
| 52 |
|
eqeq1 |
⊢ ( 𝑛 = 𝑘 → ( 𝑛 = ( 𝑠 + 1 ) ↔ 𝑘 = ( 𝑠 + 1 ) ) ) |
| 53 |
52
|
notbid |
⊢ ( 𝑛 = 𝑘 → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝑘 = ( 𝑠 + 1 ) ) ) |
| 54 |
53
|
adantl |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ( ¬ 𝑛 = ( 𝑠 + 1 ) ↔ ¬ 𝑘 = ( 𝑠 + 1 ) ) ) |
| 55 |
51 54
|
mpbird |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ¬ 𝑛 = ( 𝑠 + 1 ) ) |
| 56 |
55
|
iffalsed |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) |
| 57 |
|
simplr |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ( 𝑠 + 1 ) < 𝑘 ) |
| 58 |
|
breq2 |
⊢ ( 𝑛 = 𝑘 → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝑘 ) ) |
| 59 |
58
|
adantl |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ( ( 𝑠 + 1 ) < 𝑛 ↔ ( 𝑠 + 1 ) < 𝑘 ) ) |
| 60 |
57 59
|
mpbird |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → ( 𝑠 + 1 ) < 𝑛 ) |
| 61 |
60
|
iftrued |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = 0 ) |
| 62 |
61 7
|
eqtrdi |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) |
| 63 |
46 56 62
|
3eqtrd |
⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) ∧ 𝑛 = 𝑘 ) → if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) |
| 64 |
23 63
|
csbied |
⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑠 + 1 ) < 𝑘 ) → ⦋ 𝑘 / 𝑛 ⦌ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) |
| 65 |
64
|
ex |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 + 1 ) < 𝑘 → ⦋ 𝑘 / 𝑛 ⦌ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) ) |
| 66 |
65
|
ralrimiva |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝑠 + 1 ) < 𝑘 → ⦋ 𝑘 / 𝑛 ⦌ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) ) |
| 67 |
|
breq1 |
⊢ ( 𝑙 = ( 𝑠 + 1 ) → ( 𝑙 < 𝑘 ↔ ( 𝑠 + 1 ) < 𝑘 ) ) |
| 68 |
67
|
rspceaimv |
⊢ ( ( ( 𝑠 + 1 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 ( ( 𝑠 + 1 ) < 𝑘 → ⦋ 𝑘 / 𝑛 ⦌ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) ) → ∃ 𝑙 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 ( 𝑙 < 𝑘 → ⦋ 𝑘 / 𝑛 ⦌ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) ) |
| 69 |
22 66 68
|
syl2anc |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∃ 𝑙 ∈ ℕ0 ∀ 𝑘 ∈ ℕ0 ( 𝑙 < 𝑘 → ⦋ 𝑘 / 𝑛 ⦌ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( 0g ‘ 𝑌 ) ) ) |
| 70 |
10 18 69
|
mptnn0fsupp |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) ) finSupp ( 0g ‘ 𝑌 ) ) |
| 71 |
9 70
|
eqbrtrid |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 finSupp ( 0g ‘ 𝑌 ) ) |