Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . 3
⊢
(0g‘𝑃) ∈ V |
2 | 1 | a1i 11 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (0g‘𝑃) ∈ V) |
3 | | ovex 6577 |
. . 3
⊢ ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋)) ∈ V |
4 | 3 | a1i 11 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑛 ∈ ℕ0) → ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋)) ∈ V) |
5 | | oveq2 6557 |
. . . 4
⊢ (𝑛 = 𝑥 → (𝑀 decompPMat 𝑛) = (𝑀 decompPMat 𝑥)) |
6 | 5 | oveqd 6566 |
. . 3
⊢ (𝑛 = 𝑥 → (𝐼(𝑀 decompPMat 𝑛)𝐽) = (𝐼(𝑀 decompPMat 𝑥)𝐽)) |
7 | | oveq1 6556 |
. . 3
⊢ (𝑛 = 𝑥 → (𝑛 ↑ 𝑋) = (𝑥 ↑ 𝑋)) |
8 | 6, 7 | oveq12d 6567 |
. 2
⊢ (𝑛 = 𝑥 → ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋)) = ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋))) |
9 | | pmatcollpw1.c |
. . . . 5
⊢ 𝐶 = (𝑁 Mat 𝑃) |
10 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) |
11 | | pmatcollpw1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
12 | | simp2 1055 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐼 ∈ 𝑁) |
13 | | simp3 1056 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐽 ∈ 𝑁) |
14 | | simp13 1086 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
15 | 9, 10, 11, 12, 13, 14 | matecld 20051 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝐼𝑀𝐽) ∈ (Base‘𝑃)) |
16 | | eqid 2610 |
. . . . 5
⊢
(coe1‘(𝐼𝑀𝐽)) = (coe1‘(𝐼𝑀𝐽)) |
17 | | pmatcollpw1.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
18 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
19 | 16, 10, 17, 18 | coe1ae0 19407 |
. . . 4
⊢ ((𝐼𝑀𝐽) ∈ (Base‘𝑃) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅))) |
20 | 15, 19 | syl 17 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅))) |
21 | | simpl12 1130 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → 𝑅 ∈ Ring) |
22 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → 𝑀 ∈ 𝐵) |
23 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
24 | | 3simpc 1053 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) |
26 | 17, 9, 11 | decpmate 20390 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑥 ∈ ℕ0) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = ((coe1‘(𝐼𝑀𝐽))‘𝑥)) |
27 | 21, 22, 23, 25, 26 | syl31anc 1321 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = ((coe1‘(𝐼𝑀𝐽))‘𝑥)) |
28 | 27 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = ((coe1‘(𝐼𝑀𝐽))‘𝑥)) |
29 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) |
30 | 28, 29 | eqtrd 2644 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → (𝐼(𝑀 decompPMat 𝑥)𝐽) = (0g‘𝑅)) |
31 | 30 | oveq1d 6564 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = ((0g‘𝑅) × (𝑥 ↑ 𝑋))) |
32 | | pmatcollpw1.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (var1‘𝑅) |
33 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
34 | | pmatcollpw1.e |
. . . . . . . . . . . 12
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
35 | 17, 32, 33, 34, 10 | ply1moncl 19462 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ0)
→ (𝑥 ↑ 𝑋) ∈ (Base‘𝑃)) |
36 | 21, 23, 35 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → (𝑥 ↑ 𝑋) ∈ (Base‘𝑃)) |
37 | | pmatcollpw1.m |
. . . . . . . . . . 11
⊢ × = (
·𝑠 ‘𝑃) |
38 | 17, 10, 37, 18 | ply10s0 19447 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ↑ 𝑋) ∈ (Base‘𝑃)) → ((0g‘𝑅) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
39 | 21, 36, 38 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) →
((0g‘𝑅)
×
(𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((0g‘𝑅) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
41 | 31, 40 | eqtrd 2644 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) ∧
((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)) |
42 | 41 | ex 449 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) →
(((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅) → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃))) |
43 | 42 | imim2d 55 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → (𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)))) |
44 | 43 | ralimdva 2945 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)))) |
45 | 44 | reximdv 2999 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘(𝐼𝑀𝐽))‘𝑥) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃)))) |
46 | 20, 45 | mpd 15 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((𝐼(𝑀 decompPMat 𝑥)𝐽) × (𝑥 ↑ 𝑋)) = (0g‘𝑃))) |
47 | 2, 4, 8, 46 | mptnn0fsuppd 12660 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑛 ∈ ℕ0 ↦ ((𝐼(𝑀 decompPMat 𝑛)𝐽) × (𝑛 ↑ 𝑋))) finSupp (0g‘𝑃)) |