Step | Hyp | Ref
| Expression |
1 | | fvexd 6789 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (0g‘𝑃) ∈ V) |
2 | | ovexd 7310 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑛 ∈ ℕ0) → ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋)) ∈ V) |
3 | | oveq2 7283 |
. . . 4
⊢ (𝑛 = 𝑥 → (𝑀 decompPMat 𝑛) = (𝑀 decompPMat 𝑥)) |
4 | 3 | oveqd 7292 |
. . 3
⊢ (𝑛 = 𝑥 → (𝐼(𝑀 decompPMat 𝑛)𝐽) = (𝐼(𝑀 decompPMat 𝑥)𝐽)) |
5 | | oveq1 7282 |
. . 3
⊢ (𝑛 = 𝑥 → (𝑛 ↑ 𝑋) = (𝑥 ↑ 𝑋)) |
6 | 4, 5 | oveq12d 7293 |
. 2
⊢ (𝑛 = 𝑥 → ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋)) = ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋))) |
7 | | pmatcollpw1.c |
. . . . 5
⊢ 𝐶 = (𝑁 Mat 𝑃) |
8 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) |
9 | | pmatcollpw1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
10 | | simp2 1136 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐼 ∈ 𝑁) |
11 | | simp3 1137 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐽 ∈ 𝑁) |
12 | | simp13 1204 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
13 | 7, 8, 9, 10, 11, 12 | matecld 21575 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝐼𝑀𝐽) ∈ (Base‘𝑃)) |
14 | | eqid 2738 |
. . . . 5
⊢
(coe1‘(𝐼𝑀𝐽)) = (coe1‘(𝐼𝑀𝐽)) |
15 | | pmatcollpw1.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
16 | | eqid 2738 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
17 | 14, 8, 15, 16 | coe1ae0 21387 |
. . . 4
⊢ ((𝐼𝑀𝐽) ∈ (Base‘𝑃) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅))) |
18 | 13, 17 | syl 17 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅))) |
19 | | simpl12 1248 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → 𝑅 ∈ Ring) |
20 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → 𝑀 ∈ 𝐵) |
21 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
22 | | 3simpc 1149 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) |
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) |
24 | 15, 7, 9 | decpmate 21915 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = ((coe1‘(𝐼𝑀𝐽))‘𝑥)) |
25 | 19, 20, 21, 23, 24 | syl31anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = ((coe1‘(𝐼𝑀𝐽))‘𝑥)) |
26 | 25 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = ((coe1‘(𝐼𝑀𝐽))‘𝑥)) |
27 | | simpr 485 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) |
28 | 26, 27 | eqtrd 2778 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = (0g‘𝑅)) |
29 | 28 | oveq1d 7290 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = ((0g‘𝑅) × (𝑥 ↑ 𝑋))) |
30 | | pmatcollpw1.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (var1‘𝑅) |
31 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
32 | | pmatcollpw1.e |
. . . . . . . . . . . 12
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
33 | 15, 30, 31, 32, 8 | ply1moncl 21442 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ0)
→ (𝑥 ↑ 𝑋) ∈ (Base‘𝑃)) |
34 | 19, 21, 33 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → (𝑥 ↑ 𝑋) ∈ (Base‘𝑃)) |
35 | | pmatcollpw1.m |
. . . . . . . . . . 11
⊢ × = (
·𝑠 ‘𝑃) |
36 | 15, 8, 35, 16 | ply10s0 21427 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ↑ 𝑋) ∈ (Base‘𝑃)) → ((0g‘𝑅) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
37 | 19, 34, 36 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) →
((0g‘𝑅)
×
(𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((0g‘𝑅) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
39 | 29, 38 | eqtrd 2778 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
40 | 39 | ex 413 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) →
(((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅) → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃))) |
41 | 40 | imim2d 57 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → (𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)))) |
42 | 41 | ralimdva 3108 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)))) |
43 | 42 | reximdv 3202 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)))) |
44 | 18, 43 | mpd 15 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃))) |
45 | 1, 2, 6, 44 | mptnn0fsuppd 13718 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑛 ∈ ℕ0 ↦ ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋))) finSupp (0g‘𝑃)) |