Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . 3
⊢
(0g‘𝑅) ∈ V |
2 | 1 | a1i 11 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
3 | | mptcoe1matfsupp.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
4 | | eqid 2610 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
5 | | eqid 2610 |
. . 3
⊢
(Base‘𝐴) =
(Base‘𝐴) |
6 | | simp2 1055 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐼 ∈ 𝑁) |
7 | 6 | adantr 480 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝐼 ∈ 𝑁) |
8 | | simp3 1056 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐽 ∈ 𝑁) |
9 | 8 | adantr 480 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝐽 ∈ 𝑁) |
10 | | simp3 1056 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑂 ∈ 𝐿) |
11 | 10 | 3ad2ant1 1075 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝑂 ∈ 𝐿) |
12 | | eqid 2610 |
. . . . 5
⊢
(coe1‘𝑂) = (coe1‘𝑂) |
13 | | mptcoe1matfsupp.l |
. . . . 5
⊢ 𝐿 = (Base‘𝑄) |
14 | | mptcoe1matfsupp.q |
. . . . 5
⊢ 𝑄 = (Poly1‘𝐴) |
15 | 12, 13, 14, 5 | coe1fvalcl 19403 |
. . . 4
⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) |
16 | 11, 15 | sylan 487 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) |
17 | 3, 4, 5, 7, 9, 16 | matecld 20051 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → (𝐼((coe1‘𝑂)‘𝑘)𝐽) ∈ (Base‘𝑅)) |
18 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐴) = (0g‘𝐴) |
19 | 12, 13, 14, 18, 5 | coe1fsupp 19405 |
. . . . . 6
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) ∈ {𝑐 ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∣ 𝑐 finSupp (0g‘𝐴)}) |
20 | | elrabi 3328 |
. . . . . 6
⊢
((coe1‘𝑂) ∈ {𝑐 ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∣ 𝑐 finSupp (0g‘𝐴)} →
(coe1‘𝑂)
∈ ((Base‘𝐴)
↑𝑚 ℕ0)) |
21 | 11, 19, 20 | 3syl 18 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (coe1‘𝑂) ∈ ((Base‘𝐴) ↑𝑚
ℕ0)) |
22 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐴) ∈ V |
23 | 21, 22 | jctir 559 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ((coe1‘𝑂) ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∧ (0g‘𝐴) ∈ V)) |
24 | 12, 13, 14, 18 | coe1sfi 19404 |
. . . . 5
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) finSupp
(0g‘𝐴)) |
25 | 11, 24 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (coe1‘𝑂) finSupp
(0g‘𝐴)) |
26 | | fsuppmapnn0ub 12657 |
. . . 4
⊢
(((coe1‘𝑂) ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∧ (0g‘𝐴) ∈ V) →
((coe1‘𝑂)
finSupp (0g‘𝐴) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) |
27 | 23, 25, 26 | sylc 63 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) |
28 | | csbov 6586 |
. . . . . . . . . 10
⊢
⦋𝑥 /
𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (𝐼⦋𝑥 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝐽) |
29 | | csbfv 6143 |
. . . . . . . . . . 11
⊢
⦋𝑥 /
𝑘⦌((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝑥) |
30 | 29 | oveqi 6562 |
. . . . . . . . . 10
⊢ (𝐼⦋𝑥 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝐽) = (𝐼((coe1‘𝑂)‘𝑥)𝐽) |
31 | 28, 30 | eqtri 2632 |
. . . . . . . . 9
⊢
⦋𝑥 /
𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (𝐼((coe1‘𝑂)‘𝑥)𝐽) |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (𝐼((coe1‘𝑂)‘𝑥)𝐽)) |
33 | | oveq 6555 |
. . . . . . . . 9
⊢
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → (𝐼((coe1‘𝑂)‘𝑥)𝐽) = (𝐼(0g‘𝐴)𝐽)) |
34 | 33 | adantl 481 |
. . . . . . . 8
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝐼((coe1‘𝑂)‘𝑥)𝐽) = (𝐼(0g‘𝐴)𝐽)) |
35 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
36 | 3, 35 | mat0op 20044 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
37 | 36 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
38 | 37 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
39 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → (0g‘𝑅) = (0g‘𝑅)) |
40 | 38, 39, 6, 8, 2 | ovmpt2d 6686 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝐼(0g‘𝐴)𝐽) = (0g‘𝑅)) |
41 | 40 | ad4antr 764 |
. . . . . . . 8
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝐼(0g‘𝐴)𝐽) = (0g‘𝑅)) |
42 | 32, 34, 41 | 3eqtrd 2648 |
. . . . . . 7
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)) |
43 | 42 | exp31 628 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑠 < 𝑥 →
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) |
44 | 43 | a2d 29 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑠 < 𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) |
45 | 44 | ralimdva 2945 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) |
46 | 45 | reximdva 3000 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) |
47 | 27, 46 | mpd 15 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅))) |
48 | 2, 17, 47 | mptnn0fsupp 12659 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ (𝐼((coe1‘𝑂)‘𝑘)𝐽)) finSupp (0g‘𝑅)) |