Proof of Theorem pmatcollpwfi
Step | Hyp | Ref
| Expression |
1 | | crngring 19776 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | 1 | 3ad2ant2 1132 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
3 | | simp3 1136 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
4 | | pmatcollpw.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
5 | | pmatcollpw.c |
. . . 4
⊢ 𝐶 = (𝑁 Mat 𝑃) |
6 | | pmatcollpw.b |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
7 | | eqid 2739 |
. . . 4
⊢ (𝑁 Mat 𝑅) = (𝑁 Mat 𝑅) |
8 | | eqid 2739 |
. . . 4
⊢
(0g‘(𝑁 Mat 𝑅)) = (0g‘(𝑁 Mat 𝑅)) |
9 | 4, 5, 6, 7, 8 | decpmataa0 21898 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) |
10 | 2, 3, 9 | syl2anc 583 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) |
11 | | pmatcollpw.m |
. . . . . . 7
⊢ ∗ = (
·𝑠 ‘𝐶) |
12 | | pmatcollpw.e |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
13 | | pmatcollpw.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝑅) |
14 | | pmatcollpw.t |
. . . . . . 7
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
15 | 4, 5, 6, 11, 12, 13, 14 | pmatcollpw 21911 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
16 | 15 | ad2antrr 722 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
17 | | eqid 2739 |
. . . . . 6
⊢
(0g‘𝐶) = (0g‘𝐶) |
18 | | simp1 1134 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin) |
19 | 4, 5 | pmatring 21822 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
20 | 18, 2, 19 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐶 ∈ Ring) |
21 | | ringcmn 19801 |
. . . . . . . 8
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐶 ∈ CMnd) |
23 | 22 | ad2antrr 722 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝐶 ∈ CMnd) |
24 | 18 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ Fin) |
25 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) |
26 | 4 | ply1ring 21400 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑃 ∈ Ring) |
28 | 2 | anim1i 614 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 ∈ Ring ∧ 𝑛 ∈
ℕ0)) |
29 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
30 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
31 | 4, 13, 29, 12, 30 | ply1moncl 21423 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
32 | 28, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
33 | | simpl2 1190 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ CRing) |
34 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ 𝐵) |
35 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
36 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑁 Mat
𝑅)) = (Base‘(𝑁 Mat 𝑅)) |
37 | 4, 5, 6, 7, 36 | decpmatcl 21897 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0) → (𝑀 decompPMat 𝑛) ∈ (Base‘(𝑁 Mat 𝑅))) |
38 | 33, 34, 35, 37 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑀 decompPMat 𝑛) ∈ (Base‘(𝑁 Mat 𝑅))) |
39 | 14, 7, 36, 4, 5, 6 | mat2pmatbas0 21857 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑀 decompPMat 𝑛) ∈ (Base‘(𝑁 Mat 𝑅))) → (𝑇‘(𝑀 decompPMat 𝑛)) ∈ 𝐵) |
40 | 24, 25, 38, 39 | syl3anc 1369 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑀 decompPMat 𝑛)) ∈ 𝐵) |
41 | 30, 5, 6, 11 | matvscl 21561 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ ((𝑛 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝑇‘(𝑀 decompPMat 𝑛)) ∈ 𝐵)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
42 | 24, 27, 32, 40, 41 | syl22anc 835 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
43 | 42 | ralrimiva 3109 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ ℕ0 ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
44 | 43 | ad2antrr 722 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → ∀𝑛 ∈ ℕ0 ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
45 | | simplr 765 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝑠 ∈ ℕ0) |
46 | | fveq2 6768 |
. . . . . . . . . . . . 13
⊢ ((𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)) → (𝑇‘(𝑀 decompPMat 𝑛)) = (𝑇‘(0g‘(𝑁 Mat 𝑅)))) |
47 | 2, 18 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin)) |
48 | 47 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑅 ∈ Ring ∧
𝑁 ∈
Fin)) |
49 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(𝑁 Mat 𝑃)) = (0g‘(𝑁 Mat 𝑃)) |
50 | 14, 4, 8, 49 | 0mat2pmat 21866 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑇‘(0g‘(𝑁 Mat 𝑅))) = (0g‘(𝑁 Mat 𝑃))) |
51 | 48, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑇‘(0g‘(𝑁 Mat 𝑅))) = (0g‘(𝑁 Mat 𝑃))) |
52 | 46, 51 | sylan9eqr 2801 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → (𝑇‘(𝑀 decompPMat 𝑛)) = (0g‘(𝑁 Mat 𝑃))) |
53 | 52 | oveq2d 7284 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃)))) |
54 | 4, 5 | pmatlmod 21823 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) |
55 | 18, 2, 54 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐶 ∈ LMod) |
56 | 55 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ 𝐶 ∈
LMod) |
57 | 28 | adantlr 711 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑅 ∈ Ring ∧
𝑛 ∈
ℕ0)) |
58 | 57, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
59 | 4 | ply1crng 21350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
60 | 59 | anim2i 616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
61 | 60 | 3adant3 1130 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
62 | 5 | matsca2 21550 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 = (Scalar‘𝐶)) |
64 | 63 | eqcomd 2745 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝐶) = 𝑃) |
65 | 64 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (Scalar‘𝐶) =
𝑃) |
66 | 65 | fveq2d 6772 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
67 | 58, 66 | eleqtrrd 2843 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈
(Base‘(Scalar‘𝐶))) |
68 | 5 | eqcomi 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 Mat 𝑃) = 𝐶 |
69 | 68 | fveq2i 6771 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(𝑁 Mat 𝑃)) = (0g‘𝐶) |
70 | 69 | oveq2i 7279 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) = ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) |
71 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
72 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
73 | 71, 11, 72, 17 | lmodvs0 20138 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
74 | 70, 73 | eqtrid 2791 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) =
(0g‘𝐶)) |
75 | 56, 67, 74 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) =
(0g‘𝐶)) |
76 | 75 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) =
(0g‘𝐶)) |
77 | 53, 76 | eqtrd 2779 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶)) |
78 | 77 | ex 412 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ((𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶))) |
79 | 78 | imim2d 57 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ((𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → (𝑠 < 𝑛 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶)))) |
80 | 79 | ralimdva 3104 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) →
(∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶)))) |
81 | 80 | imp 406 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶))) |
82 | 6, 17, 23, 44, 45, 81 | gsummptnn0fz 19568 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → (𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
83 | 16, 82 | eqtrd 2779 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
84 | 83 | ex 412 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) →
(∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))))) |
85 | 84 | reximdva 3204 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ∃𝑠 ∈ ℕ0 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))))) |
86 | 10, 85 | mpd 15 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |