Proof of Theorem chfacfisf
Step | Hyp | Ref
| Expression |
1 | | chfacfisf.p |
. . . . . . . . 9
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | chfacfisf.y |
. . . . . . . . 9
⊢ 𝑌 = (𝑁 Mat 𝑃) |
3 | 1, 2 | pmatring 20905 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
4 | 3 | 3adant3 1123 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
5 | | ringgrp 18939 |
. . . . . . 7
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp) |
7 | 6 | adantr 474 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑌 ∈ Grp) |
8 | | eqid 2778 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
9 | | chfacfisf.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑌) |
10 | 8, 9 | ring0cl 18956 |
. . . . . . 7
⊢ (𝑌 ∈ Ring → 0 ∈
(Base‘𝑌)) |
11 | 4, 10 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 0 ∈ (Base‘𝑌)) |
12 | 11 | adantr 474 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 0 ∈ (Base‘𝑌)) |
13 | 4 | adantr 474 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑌 ∈ Ring) |
14 | | chfacfisf.t |
. . . . . . . 8
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
15 | | chfacfisf.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
16 | | chfacfisf.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐴) |
17 | 14, 15, 16, 1, 2 | mat2pmatbas 20938 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
18 | 17 | adantr 474 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
19 | | 3simpa 1139 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
20 | | elmapi 8162 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵) |
21 | 20 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵) |
22 | | nnnn0 11650 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
23 | | nn0uz 12028 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
24 | 22, 23 | syl6eleq 2869 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
(ℤ≥‘0)) |
25 | | eluzfz1 12665 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑠)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ℕ → 0 ∈
(0...𝑠)) |
27 | 26 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → 0 ∈ (0...𝑠)) |
28 | 21, 27 | ffvelrnd 6624 |
. . . . . . . . 9
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑏‘0) ∈ 𝐵) |
29 | 19, 28 | anim12i 606 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘0) ∈ 𝐵)) |
30 | | df-3an 1073 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘0) ∈ 𝐵)) |
31 | 29, 30 | sylibr 226 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵)) |
32 | 14, 15, 16, 1, 2 | mat2pmatbas 20938 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
34 | | chfacfisf.r |
. . . . . . 7
⊢ × =
(.r‘𝑌) |
35 | 8, 34 | ringcl 18948 |
. . . . . 6
⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
36 | 13, 18, 33, 35 | syl3anc 1439 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
37 | | chfacfisf.s |
. . . . . 6
⊢ − =
(-g‘𝑌) |
38 | 8, 37 | grpsubcl 17882 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 0 ∈
(Base‘𝑌) ∧
((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌)) |
39 | 7, 12, 36, 38 | syl3anc 1439 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌)) |
40 | 39 | ad2antrr 716 |
. . 3
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌)) |
41 | 22 | adantr 474 |
. . . . . . . . 9
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → 𝑠 ∈ ℕ0) |
42 | 19, 41 | anim12i 606 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈
ℕ0)) |
43 | | df-3an 1073 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
↔ ((𝑁 ∈ Fin ∧
𝑅 ∈ Ring) ∧ 𝑠 ∈
ℕ0)) |
44 | 42, 43 | sylibr 226 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈
ℕ0)) |
45 | | eluzfz2 12666 |
. . . . . . . . . . 11
⊢ (𝑠 ∈
(ℤ≥‘0) → 𝑠 ∈ (0...𝑠)) |
46 | 24, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℕ → 𝑠 ∈ (0...𝑠)) |
47 | 46 | anim1i 608 |
. . . . . . . . 9
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑠 ∈ (0...𝑠) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) |
48 | 47 | ancomd 455 |
. . . . . . . 8
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠))) |
49 | 48 | adantl 475 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠))) |
50 | 15, 16, 1, 2, 14 | m2pmfzmap 20959 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ (𝑏 ∈ (𝐵 ↑𝑚
(0...𝑠)) ∧ 𝑠 ∈ (0...𝑠))) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) |
51 | 44, 49, 50 | syl2anc 579 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) |
52 | 51 | adantr 474 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) |
53 | 52 | ad2antrr 716 |
. . . 4
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) |
54 | 12 | ad4antr 722 |
. . . . 5
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ (𝑠 + 1) < 𝑛) → 0 ∈ (Base‘𝑌)) |
55 | | nn0re 11652 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
56 | 55 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ 𝑛 ∈
ℝ) |
57 | | peano2nn 11388 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ) |
58 | 57 | nnred 11391 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℝ) |
59 | 58 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (𝑠 + 1) ∈
ℝ) |
60 | 56, 59 | lenltd 10522 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ≤ (𝑠 + 1) ↔ ¬ (𝑠 + 1) < 𝑛)) |
61 | | nesym 3025 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 + 1) ≠ 𝑛 ↔ ¬ 𝑛 = (𝑠 + 1)) |
62 | | ltlen 10477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) →
(𝑛 < (𝑠 + 1) ↔ (𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛))) |
63 | 55, 58, 62 | syl2anr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (𝑛 < (𝑠 + 1) ↔ (𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛))) |
64 | 63 | biimprd 240 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ ((𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛) → 𝑛 < (𝑠 + 1))) |
65 | 64 | expcomd 408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ ((𝑠 + 1) ≠ 𝑛 → (𝑛 ≤ (𝑠 + 1) → 𝑛 < (𝑠 + 1)))) |
66 | 61, 65 | syl5bir 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (¬ 𝑛 = (𝑠 + 1) → (𝑛 ≤ (𝑠 + 1) → 𝑛 < (𝑠 + 1)))) |
67 | 66 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ≤ (𝑠 + 1) → (¬ 𝑛 = (𝑠 + 1) → 𝑛 < (𝑠 + 1)))) |
68 | 60, 67 | sylbird 252 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (¬ (𝑠 + 1) <
𝑛 → (¬ 𝑛 = (𝑠 + 1) → 𝑛 < (𝑠 + 1)))) |
69 | 68 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (¬ 𝑛 = (𝑠 + 1) → (¬ (𝑠 + 1) < 𝑛 → 𝑛 < (𝑠 + 1)))) |
70 | 69 | impd 400 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))) |
71 | 70 | ex 403 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0
→ ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))) |
72 | 71 | ad2antrl 718 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ0 → ((¬
𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))) |
73 | 72 | imp 397 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → ((¬
𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))) |
74 | 73 | adantr 474 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))) |
75 | 3, 5 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Grp) |
76 | 75 | 3adant3 1123 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp) |
77 | 76 | ad4antr 722 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑌 ∈ Grp) |
78 | 19 | ad4antr 722 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
79 | 21 | ad4antlr 723 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑏:(0...𝑠)⟶𝐵) |
80 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 0 → 𝑛 = 0) |
81 | 80 | necon3bi 2995 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑛 = 0 → 𝑛 ≠ 0) |
82 | 81 | anim2i 610 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
(𝑛 ∈
ℕ0 ∧ 𝑛
≠ 0)) |
83 | | elnnne0 11658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0
∧ 𝑛 ≠
0)) |
84 | 82, 83 | sylibr 226 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
𝑛 ∈
ℕ) |
85 | | nnm1nn0 11685 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
(𝑛 − 1) ∈
ℕ0) |
87 | 86 | adantll 704 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (𝑛 − 1) ∈
ℕ0) |
88 | 87 | adantr 474 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ∈
ℕ0) |
89 | 41 | ad4antlr 723 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℕ0) |
90 | 63 | simprbda 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑛 ≤ (𝑠 + 1)) |
91 | 56 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ ℝ) |
92 | | 1red 10377 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 1 ∈
ℝ) |
93 | | nnre 11382 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℝ) |
94 | 93 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℝ) |
95 | 91, 92, 94 | lesubaddd 10972 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → ((𝑛 − 1) ≤ 𝑠 ↔ 𝑛 ≤ (𝑠 + 1))) |
96 | 90, 95 | mpbird 249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ≤ 𝑠) |
97 | 96 | exp31 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0
→ (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠))) |
98 | 97 | ad2antrl 718 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠))) |
99 | 98 | imp 397 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠)) |
100 | 99 | adantr 474 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠)) |
101 | 100 | imp 397 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ≤ 𝑠) |
102 | | elfz2nn0 12749 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 1) ∈ (0...𝑠) ↔ ((𝑛 − 1) ∈ ℕ0 ∧
𝑠 ∈
ℕ0 ∧ (𝑛 − 1) ≤ 𝑠)) |
103 | 88, 89, 101, 102 | syl3anbrc 1400 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ∈ (0...𝑠)) |
104 | 79, 103 | ffvelrnd 6624 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑏‘(𝑛 − 1)) ∈ 𝐵) |
105 | | df-3an 1073 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵)) |
106 | 78, 104, 105 | sylanbrc 578 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵)) |
107 | 14, 15, 16, 1, 2 | mat2pmatbas 20938 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵) → (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌)) |
108 | 106, 107 | syl 17 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌)) |
109 | 13 | ad2antrr 716 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑌 ∈ Ring) |
110 | 18 | ad2antrr 716 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
111 | 44 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈
ℕ0)) |
112 | | simprr 763 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) |
113 | 112 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) |
114 | | simplr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ ℕ0) |
115 | 22 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℕ0) |
116 | | nn0z 11752 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
117 | | nnz 11751 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℤ) |
118 | | zleltp1 11780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑛 ≤ 𝑠 ↔ 𝑛 < (𝑠 + 1))) |
119 | 116, 117,
118 | syl2anr 590 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ≤ 𝑠 ↔ 𝑛 < (𝑠 + 1))) |
120 | 119 | biimpar 471 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑛 ≤ 𝑠) |
121 | | elfz2nn0 12749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (0...𝑠) ↔ (𝑛 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝑛 ≤ 𝑠)) |
122 | 114, 115,
120, 121 | syl3anbrc 1400 |
. . . . . . . . . . . . . . 15
⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ (0...𝑠)) |
123 | 122 | exp31 412 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0
→ (𝑛 < (𝑠 + 1) → 𝑛 ∈ (0...𝑠)))) |
124 | 123 | ad2antrl 718 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → 𝑛 ∈ (0...𝑠)))) |
125 | 124 | imp31 410 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ (0...𝑠)) |
126 | 15, 16, 1, 2, 14 | m2pmfzmap 20959 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0)
∧ (𝑏 ∈ (𝐵 ↑𝑚
(0...𝑠)) ∧ 𝑛 ∈ (0...𝑠))) → (𝑇‘(𝑏‘𝑛)) ∈ (Base‘𝑌)) |
127 | 111, 113,
125, 126 | syl12anc 827 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘(𝑏‘𝑛)) ∈ (Base‘𝑌)) |
128 | 8, 34 | ringcl 18948 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘𝑛)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌)) |
129 | 109, 110,
127, 128 | syl3anc 1439 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌)) |
130 | 129 | adantlr 705 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌)) |
131 | 8, 37 | grpsubcl 17882 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Grp ∧ (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌) ∧ ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌)) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌)) |
132 | 77, 108, 130, 131 | syl3anc 1439 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌)) |
133 | 132 | ex 403 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (𝑛 < (𝑠 + 1) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌))) |
134 | 74, 133 | syld 47 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌))) |
135 | 134 | impl 449 |
. . . . 5
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌)) |
136 | 54, 135 | ifclda 4341 |
. . . 4
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))) ∈ (Base‘𝑌)) |
137 | 53, 136 | ifclda 4341 |
. . 3
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) ∈ (Base‘𝑌)) |
138 | 40, 137 | ifclda 4341 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) ∈ (Base‘𝑌)) |
139 | | chfacfisf.g |
. 2
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
140 | 138, 139 | fmptd 6648 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) |