Step | Hyp | Ref
| Expression |
1 | | cayleyhamilton.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | cayleyhamilton.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
3 | | cayleyhamilton.0 |
. . . 4
⊢ 0 =
(0g‘𝐴) |
4 | | cayleyhamilton.c |
. . . 4
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
5 | | cayleyhamilton.k |
. . . 4
⊢ 𝐾 = (coe1‘(𝐶‘𝑀)) |
6 | | cayleyhamilton.m |
. . . 4
⊢ ∗ = (
·𝑠 ‘𝐴) |
7 | | cayleyhamilton.e |
. . . 4
⊢ ↑ =
(.g‘(mulGrp‘𝐴)) |
8 | 1, 2, 3, 4, 5, 6, 7 | cayleyhamilton 22020 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ) |
9 | 8 | adantr 480 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ) |
10 | | nfv 1920 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) |
11 | | nfcv 2908 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑃 |
12 | | nfcv 2908 |
. . . . . . . . . 10
⊢
Ⅎ𝑛
Σg |
13 | | nfmpt1 5186 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))) |
14 | 11, 12, 13 | nfov 7298 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) |
15 | 14 | nfeq2 2925 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) |
16 | 10, 15 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑛(((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) |
17 | | crngring 19776 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
18 | 17 | 3ad2ant2 1132 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
19 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → 𝑅 ∈ Ring) |
20 | | cayleyhamilton1.p |
. . . . . . . . . . . . 13
⊢ 𝑃 = (Poly1‘𝑅) |
21 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑃) =
(Base‘𝑃) |
22 | 4, 1, 2, 20, 21 | chpmatply1 21962 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
24 | | cayleyhamilton1.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (var1‘𝑅) |
25 | | cayleyhamilton1.e |
. . . . . . . . . . . 12
⊢ 𝐸 =
(.g‘(mulGrp‘𝑃)) |
26 | | cayleyhamilton1.l |
. . . . . . . . . . . 12
⊢ 𝐿 = (Base‘𝑅) |
27 | | cayleyhamilton1.m |
. . . . . . . . . . . 12
⊢ · = (
·𝑠 ‘𝑃) |
28 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
29 | | elmapi 8611 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ 𝐹:ℕ0⟶𝐿) |
30 | | ffvelrn 6953 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ0⟶𝐿 ∧ 𝑛 ∈ ℕ0) → (𝐹‘𝑛) ∈ 𝐿) |
31 | 30 | ralrimiva 3109 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℕ0⟶𝐿 → ∀𝑛 ∈ ℕ0
(𝐹‘𝑛) ∈ 𝐿) |
32 | 29, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ ∀𝑛 ∈
ℕ0 (𝐹‘𝑛) ∈ 𝐿) |
33 | 32 | ad2antrl 724 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → ∀𝑛 ∈ ℕ0
(𝐹‘𝑛) ∈ 𝐿) |
34 | 29 | feqmptd 6831 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ 𝐹 = (𝑛 ∈ ℕ0
↦ (𝐹‘𝑛))) |
35 | | cayleyhamilton1.z |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 = (0g‘𝑅) |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ 𝑍 =
(0g‘𝑅)) |
37 | 34, 36 | breq12d 5091 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ (𝐹 finSupp 𝑍 ↔ (𝑛 ∈ ℕ0 ↦ (𝐹‘𝑛)) finSupp (0g‘𝑅))) |
38 | 37 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍) → (𝑛 ∈ ℕ0 ↦ (𝐹‘𝑛)) finSupp (0g‘𝑅)) |
39 | 38 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝑛 ∈ ℕ0 ↦ (𝐹‘𝑛)) finSupp (0g‘𝑅)) |
40 | 20, 21, 24, 25, 19, 26, 27, 28, 33, 39 | gsumsmonply1 21455 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) ∈ (Base‘𝑃)) |
41 | | fveq2 6768 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛)) |
42 | | oveq1 7275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑛 → (𝑖𝐸𝑋) = (𝑛𝐸𝑋)) |
43 | 41, 42 | oveq12d 7286 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → ((𝐹‘𝑖) · (𝑖𝐸𝑋)) = ((𝐹‘𝑛) · (𝑛𝐸𝑋))) |
44 | 43 | cbvmptv 5191 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ0
↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋))) = (𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))) |
45 | 44 | oveq2i 7279 |
. . . . . . . . . . . . 13
⊢ (𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) |
46 | 45 | fveq2i 6771 |
. . . . . . . . . . . 12
⊢
(coe1‘(𝑃 Σg (𝑖 ∈ ℕ0
↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋))))) = (coe1‘(𝑃 Σg
(𝑛 ∈
ℕ0 ↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) |
47 | 20, 21, 5, 46 | ply1coe1eq 21450 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝐶‘𝑀) ∈ (Base‘𝑃) ∧ (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) ∈ (Base‘𝑃)) → (∀𝑚 ∈ ℕ0 (𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚) ↔ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))))) |
48 | 19, 23, 40, 47 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (∀𝑚 ∈ ℕ0
(𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚) ↔ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))))) |
49 | | fveq2 6768 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝐾‘𝑚) = (𝐾‘𝑛)) |
50 | | fveq2 6768 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛)) |
51 | 49, 50 | eqeq12d 2755 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → ((𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚) ↔ (𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛))) |
52 | 51 | rspcva 3558 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℕ0 (𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚)) → (𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛)) |
53 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) ∧ (𝑛 ∈ ℕ0 ∧ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)))) → (𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛)) |
54 | 18 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0
∧ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍))) → 𝑅 ∈ Ring) |
55 | | ffvelrn 6953 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹:ℕ0⟶𝐿 ∧ 𝑖 ∈ ℕ0) → (𝐹‘𝑖) ∈ 𝐿) |
56 | 55 | ralrimiva 3109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:ℕ0⟶𝐿 → ∀𝑖 ∈ ℕ0
(𝐹‘𝑖) ∈ 𝐿) |
57 | 29, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ ∀𝑖 ∈
ℕ0 (𝐹‘𝑖) ∈ 𝐿) |
58 | 57 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → ∀𝑖 ∈ ℕ0
(𝐹‘𝑖) ∈ 𝐿) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0
∧ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍))) → ∀𝑖 ∈ ℕ0
(𝐹‘𝑖) ∈ 𝐿) |
60 | 29 | feqmptd 6831 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ 𝐹 = (𝑖 ∈ ℕ0
↦ (𝐹‘𝑖))) |
61 | 60 | breq1d 5088 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 ∈ (𝐿 ↑m ℕ0)
→ (𝐹 finSupp 𝑍 ↔ (𝑖 ∈ ℕ0 ↦ (𝐹‘𝑖)) finSupp 𝑍)) |
62 | 61 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍) → (𝑖 ∈ ℕ0 ↦ (𝐹‘𝑖)) finSupp 𝑍) |
63 | 62 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝑖 ∈ ℕ0 ↦ (𝐹‘𝑖)) finSupp 𝑍) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0
∧ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍))) → (𝑖 ∈ ℕ0 ↦ (𝐹‘𝑖)) finSupp 𝑍) |
65 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0
∧ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍))) → 𝑛 ∈ ℕ0) |
66 | 20, 21, 24, 25, 54, 26, 27, 35, 59, 64, 65 | gsummoncoe1 21456 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0
∧ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍))) →
((coe1‘(𝑃
Σg (𝑖 ∈ ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) = ⦋𝑛 / 𝑖⦌(𝐹‘𝑖)) |
67 | | csbfv 6813 |
. . . . . . . . . . . . . . . . . . 19
⊢
⦋𝑛 /
𝑖⦌(𝐹‘𝑖) = (𝐹‘𝑛) |
68 | 66, 67 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0
∧ ((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍))) →
((coe1‘(𝑃
Σg (𝑖 ∈ ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) = (𝐹‘𝑛)) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) ∧ (𝑛 ∈ ℕ0 ∧ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)))) →
((coe1‘(𝑃
Σg (𝑖 ∈ ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) = (𝐹‘𝑛)) |
70 | 53, 69 | eqtrd 2779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) ∧ (𝑛 ∈ ℕ0 ∧ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)))) → (𝐾‘𝑛) = (𝐹‘𝑛)) |
71 | 70 | exp32 420 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) → (𝑛 ∈ ℕ0 → (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝐾‘𝑛) = (𝐹‘𝑛)))) |
72 | 71 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ ((𝐾‘𝑛) =
((coe1‘(𝑃
Σg (𝑖 ∈ ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝐾‘𝑛) = (𝐹‘𝑛)))) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℕ0 (𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚)) → ((𝐾‘𝑛) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝐾‘𝑛) = (𝐹‘𝑛)))) |
74 | 52, 73 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ0
∧ ∀𝑚 ∈
ℕ0 (𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚)) → (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (𝐾‘𝑛) = (𝐹‘𝑛))) |
75 | 74 | com12 32 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → ((𝑛 ∈ ℕ0 ∧
∀𝑚 ∈
ℕ0 (𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚)) → (𝐾‘𝑛) = (𝐹‘𝑛))) |
76 | 75 | expcomd 416 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → (∀𝑚 ∈ ℕ0
(𝐾‘𝑚) = ((coe1‘(𝑃 Σg
(𝑖 ∈
ℕ0 ↦ ((𝐹‘𝑖) · (𝑖𝐸𝑋)))))‘𝑚) → (𝑛 ∈ ℕ0 → (𝐾‘𝑛) = (𝐹‘𝑛)))) |
77 | 48, 76 | sylbird 259 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → ((𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) → (𝑛 ∈ ℕ0 → (𝐾‘𝑛) = (𝐹‘𝑛)))) |
78 | 77 | imp31 417 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) ∧ 𝑛 ∈ ℕ0) → (𝐾‘𝑛) = (𝐹‘𝑛)) |
79 | 78 | oveq1d 7283 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) ∧ 𝑛 ∈ ℕ0) → ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀))) |
80 | 16, 79 | mpteq2da 5176 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) → (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) |
81 | 80 | oveq2d 7284 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) → (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀))))) |
82 | 81 | eqeq1d 2741 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) → ((𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ↔ (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )) |
83 | 82 | biimpd 228 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) ∧ (𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋))))) → ((𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 → (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )) |
84 | 83 | ex 412 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → ((𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) → ((𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 → (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))) |
85 | 9, 84 | mpid 44 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0)
∧ 𝐹 finSupp 𝑍)) → ((𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) → (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )) |