Step | Hyp | Ref
| Expression |
1 | | cayhamlem1.0 |
. . . 4
⊢ 0 =
(0g‘𝑌) |
2 | | fvex 6113 |
. . . 4
⊢
(0g‘𝑌) ∈ V |
3 | 1, 2 | eqeltri 2684 |
. . 3
⊢ 0 ∈
V |
4 | 3 | a1i 11 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 0 ∈ V) |
5 | | ovex 6577 |
. . 3
⊢ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ V |
6 | 5 | a1i 11 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ V) |
7 | | nnnn0 11176 |
. . . . 5
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
8 | 7 | ad2antrl 760 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑠 ∈ ℕ0) |
9 | | 1nn0 11185 |
. . . . 5
⊢ 1 ∈
ℕ0 |
10 | 9 | a1i 11 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 1 ∈
ℕ0) |
11 | 8, 10 | nn0addcld 11232 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
12 | | vex 3176 |
. . . . . . 7
⊢ 𝑘 ∈ V |
13 | | csbov12g 6587 |
. . . . . . . 8
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = (⦋𝑘 / 𝑖⦌(𝑖 ↑ (𝑇‘𝑀)) × ⦋𝑘 / 𝑖⦌(𝐺‘𝑖))) |
14 | | nfcvd 2752 |
. . . . . . . . . 10
⊢ (𝑘 ∈ V →
Ⅎ𝑖(𝑘 ↑ (𝑇‘𝑀))) |
15 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝑖 ↑ (𝑇‘𝑀)) = (𝑘 ↑ (𝑇‘𝑀))) |
16 | 14, 15 | csbiegf 3523 |
. . . . . . . . 9
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌(𝑖 ↑ (𝑇‘𝑀)) = (𝑘 ↑ (𝑇‘𝑀))) |
17 | | csbfv 6143 |
. . . . . . . . . 10
⊢
⦋𝑘 /
𝑖⦌(𝐺‘𝑖) = (𝐺‘𝑘) |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌(𝐺‘𝑖) = (𝐺‘𝑘)) |
19 | 16, 18 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 ∈ V →
(⦋𝑘 / 𝑖⦌(𝑖 ↑ (𝑇‘𝑀)) × ⦋𝑘 / 𝑖⦌(𝐺‘𝑖)) = ((𝑘 ↑ (𝑇‘𝑀)) × (𝐺‘𝑘))) |
20 | 13, 19 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = ((𝑘 ↑ (𝑇‘𝑀)) × (𝐺‘𝑘))) |
21 | 12, 20 | mp1i 13 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = ((𝑘 ↑ (𝑇‘𝑀)) × (𝐺‘𝑘))) |
22 | | simplll 794 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
23 | | simpllr 795 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) |
24 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → 𝑠 ∈ ℕ0) |
25 | 24 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → 𝑠 ∈
ℕ0) |
26 | 25 | nn0zd 11356 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → 𝑠 ∈
ℤ) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑠 ∈ ℤ) |
28 | | 2z 11286 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
29 | 28 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 2 ∈ ℤ) |
30 | 27, 29 | zaddcld 11362 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 + 2) ∈ ℤ) |
31 | | simplr 788 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ ℕ0) |
32 | 31 | nn0zd 11356 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ ℤ) |
33 | | peano2nn0 11210 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ0
→ (𝑠 + 1) ∈
ℕ0) |
34 | 7, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ0) |
35 | 34 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
36 | 35 | nn0zd 11356 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑠 + 1) ∈ ℤ) |
37 | | nn0z 11277 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
38 | | zltp1le 11304 |
. . . . . . . . . . 11
⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑠 + 1) < 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
39 | 36, 37, 38 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 1) < 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
40 | 39 | biimpa 500 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑠 + 1) + 1) ≤ 𝑘) |
41 | | nncn 10905 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) |
42 | | add1p1 11160 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
44 | 43 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → (((𝑠 + 1) + 1) ≤ 𝑘 ↔ (𝑠 + 2) ≤ 𝑘)) |
45 | 44 | bicomd 212 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
46 | 45 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
47 | 46 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
48 | 47 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘)) |
49 | 40, 48 | mpbird 246 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 + 2) ≤ 𝑘) |
50 | | eluz2 11569 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘(𝑠 + 2)) ↔ ((𝑠 + 2) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝑘)) |
51 | 30, 32, 49, 50 | syl3anbrc 1239 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ (ℤ≥‘(𝑠 + 2))) |
52 | | cayhamlem1.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
53 | | cayhamlem1.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐴) |
54 | | cayhamlem1.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
55 | | cayhamlem1.y |
. . . . . . . 8
⊢ 𝑌 = (𝑁 Mat 𝑃) |
56 | | cayhamlem1.r |
. . . . . . . 8
⊢ × =
(.r‘𝑌) |
57 | | cayhamlem1.s |
. . . . . . . 8
⊢ − =
(-g‘𝑌) |
58 | | cayhamlem1.t |
. . . . . . . 8
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
59 | | cayhamlem1.g |
. . . . . . . 8
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
60 | | cayhamlem1.e |
. . . . . . . 8
⊢ ↑ =
(.g‘(mulGrp‘𝑌)) |
61 | 52, 53, 54, 55, 56, 57, 1, 58, 59, 60 | chfacfpmmul0 20486 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ 𝑘 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝑘 ↑ (𝑇‘𝑀)) × (𝐺‘𝑘)) = 0 ) |
62 | 22, 23, 51, 61 | syl3anc 1318 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑘 ↑ (𝑇‘𝑀)) × (𝐺‘𝑘)) = 0 ) |
63 | 21, 62 | eqtrd 2644 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ) |
64 | 63 | ex 449 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 )) |
65 | 64 | ralrimiva 2949 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ∀𝑘 ∈ ℕ0
((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 )) |
66 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = (𝑠 + 1) → (𝑥 < 𝑘 ↔ (𝑠 + 1) < 𝑘)) |
67 | 66 | imbi1d 330 |
. . . . 5
⊢ (𝑥 = (𝑠 + 1) → ((𝑥 < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ) ↔ ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ))) |
68 | 67 | ralbidv 2969 |
. . . 4
⊢ (𝑥 = (𝑠 + 1) → (∀𝑘 ∈ ℕ0 (𝑥 < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ) ↔ ∀𝑘 ∈ ℕ0
((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ))) |
69 | 68 | rspcev 3282 |
. . 3
⊢ (((𝑠 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 ((𝑠 +
1) < 𝑘 →
⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 )) → ∃𝑥 ∈ ℕ0
∀𝑘 ∈
ℕ0 (𝑥 <
𝑘 →
⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 )) |
70 | 11, 65, 69 | syl2anc 691 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ∃𝑥 ∈ ℕ0
∀𝑘 ∈
ℕ0 (𝑥 <
𝑘 →
⦋𝑘 / 𝑖⦌((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 )) |
71 | 4, 6, 70 | mptnn0fsupp 12659 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))) finSupp 0 ) |