Proof of Theorem pmatcollpwfi
Step | Hyp | Ref
| Expression |
1 | | crngring 18381 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | 1 | 3ad2ant2 1076 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
3 | | simp3 1056 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
4 | | pmatcollpw.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
5 | | pmatcollpw.c |
. . . 4
⊢ 𝐶 = (𝑁 Mat 𝑃) |
6 | | pmatcollpw.b |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
7 | | eqid 2610 |
. . . 4
⊢ (𝑁 Mat 𝑅) = (𝑁 Mat 𝑅) |
8 | | eqid 2610 |
. . . 4
⊢
(0g‘(𝑁 Mat 𝑅)) = (0g‘(𝑁 Mat 𝑅)) |
9 | 4, 5, 6, 7, 8 | decpmataa0 20392 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) |
10 | 2, 3, 9 | syl2anc 691 |
. 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 20405 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
16 | 15 | ad2antrr 758 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
17 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑛((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) |
18 | | nfra1 2925 |
. . . . . . 7
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) |
19 | 17, 18 | nfan 1816 |
. . . . . 6
⊢
Ⅎ𝑛(((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) |
20 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐶) = (0g‘𝐶) |
21 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin) |
22 | 4, 5 | pmatring 20317 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
23 | 21, 2, 22 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐶 ∈ Ring) |
24 | | ringcmn 18404 |
. . . . . . . 8
⊢ (𝐶 ∈ Ring → 𝐶 ∈ CMnd) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐶 ∈ CMnd) |
26 | 25 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝐶 ∈ CMnd) |
27 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ Fin) |
28 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring) |
29 | 4 | ply1ring 19439 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑃 ∈ Ring) |
31 | 2 | anim1i 590 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑅 ∈ Ring ∧ 𝑛 ∈
ℕ0)) |
32 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
33 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
34 | 4, 13, 32, 12, 33 | ply1moncl 19462 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
35 | 31, 34 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
36 | | simpl2 1058 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ CRing) |
37 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ 𝐵) |
38 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑁 Mat
𝑅)) = (Base‘(𝑁 Mat 𝑅)) |
40 | 4, 5, 6, 7, 39 | decpmatcl 20391 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0) → (𝑀 decompPMat 𝑛) ∈ (Base‘(𝑁 Mat 𝑅))) |
41 | 36, 37, 38, 40 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑀 decompPMat 𝑛) ∈ (Base‘(𝑁 Mat 𝑅))) |
42 | 14, 7, 39, 4, 5, 6 | mat2pmatbas0 20351 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑀 decompPMat 𝑛) ∈ (Base‘(𝑁 Mat 𝑅))) → (𝑇‘(𝑀 decompPMat 𝑛)) ∈ 𝐵) |
43 | 27, 28, 41, 42 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑀 decompPMat 𝑛)) ∈ 𝐵) |
44 | 33, 5, 6, 11 | matvscl 20056 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ ((𝑛 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝑇‘(𝑀 decompPMat 𝑛)) ∈ 𝐵)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
45 | 27, 30, 35, 43, 44 | syl22anc 1319 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
46 | 45 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ ℕ0 ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
47 | 46 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → ∀𝑛 ∈ ℕ0 ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) ∈ 𝐵) |
48 | | simpr 476 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) → 𝑠 ∈
ℕ0) |
49 | 48 | adantr 480 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝑠 ∈ ℕ0) |
50 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ ((𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)) → (𝑇‘(𝑀 decompPMat 𝑛)) = (𝑇‘(0g‘(𝑁 Mat 𝑅)))) |
51 | 2, 21 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin)) |
52 | 51 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑅 ∈ Ring ∧
𝑁 ∈
Fin)) |
53 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(𝑁 Mat 𝑃)) = (0g‘(𝑁 Mat 𝑃)) |
54 | 14, 4, 8, 53 | 0mat2pmat 20360 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → (𝑇‘(0g‘(𝑁 Mat 𝑅))) = (0g‘(𝑁 Mat 𝑃))) |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑇‘(0g‘(𝑁 Mat 𝑅))) = (0g‘(𝑁 Mat 𝑃))) |
56 | 50, 55 | sylan9eqr 2666 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → (𝑇‘(𝑀 decompPMat 𝑛)) = (0g‘(𝑁 Mat 𝑃))) |
57 | 56 | oveq2d 6565 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃)))) |
58 | 4, 5 | pmatlmod 20318 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) |
59 | 21, 2, 58 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐶 ∈ LMod) |
60 | 59 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ 𝐶 ∈
LMod) |
61 | 31 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑅 ∈ Ring ∧
𝑛 ∈
ℕ0)) |
62 | 61, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈ (Base‘𝑃)) |
63 | 4 | ply1crng 19389 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
64 | 63 | anim2i 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
65 | 64 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
66 | 5 | matsca2 20045 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝐶)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 = (Scalar‘𝐶)) |
68 | 67 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝐶) = 𝑃) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (Scalar‘𝐶) =
𝑃) |
70 | 69 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (Base‘(Scalar‘𝐶)) = (Base‘𝑃)) |
71 | 62, 70 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ↑ 𝑋) ∈
(Base‘(Scalar‘𝐶))) |
72 | 5 | eqcomi 2619 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 Mat 𝑃) = 𝐶 |
73 | 72 | fveq2i 6106 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(𝑁 Mat 𝑃)) = (0g‘𝐶) |
74 | 73 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) = ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) |
75 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Scalar‘𝐶) =
(Scalar‘𝐶) |
76 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶)) |
77 | 75, 11, 76, 20 | lmodvs0 18720 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘𝐶)) =
(0g‘𝐶)) |
78 | 74, 77 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ LMod ∧ (𝑛 ↑ 𝑋) ∈ (Base‘(Scalar‘𝐶))) → ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) =
(0g‘𝐶)) |
79 | 60, 71, 78 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) =
(0g‘𝐶)) |
80 | 79 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ((𝑛 ↑ 𝑋) ∗
(0g‘(𝑁 Mat
𝑃))) =
(0g‘𝐶)) |
81 | 57, 80 | eqtrd 2644 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
∧ (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶)) |
82 | 81 | ex 449 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ((𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶))) |
83 | 82 | imim2d 55 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ((𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → (𝑠 < 𝑛 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶)))) |
84 | 83 | ralimdva 2945 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) →
(∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶)))) |
85 | 84 | imp 444 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → ∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))) = (0g‘𝐶))) |
86 | 19, 6, 20, 26, 47, 49, 85 | gsummptnn0fz 18205 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → (𝐶 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
87 | 16, 86 | eqtrd 2644 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧
∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅)))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |
88 | 87 | ex 449 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) →
(∀𝑛 ∈
ℕ0 (𝑠 <
𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))))) |
89 | 88 | reximdva 3000 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ0 ∀𝑛 ∈ ℕ0
(𝑠 < 𝑛 → (𝑀 decompPMat 𝑛) = (0g‘(𝑁 Mat 𝑅))) → ∃𝑠 ∈ ℕ0 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))))) |
90 | 10, 89 | mpd 15 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) |