| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvexd 6920 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (0g‘𝑅) ∈ V) | 
| 2 |  | mptcoe1matfsupp.a | . . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 3 |  | eqid 2736 | . . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 4 |  | eqid 2736 | . . 3
⊢
(Base‘𝐴) =
(Base‘𝐴) | 
| 5 |  | simp2 1137 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐼 ∈ 𝑁) | 
| 6 | 5 | adantr 480 | . . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝐼 ∈ 𝑁) | 
| 7 |  | simp3 1138 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝐽 ∈ 𝑁) | 
| 8 | 7 | adantr 480 | . . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝐽 ∈ 𝑁) | 
| 9 |  | simp3 1138 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑂 ∈ 𝐿) | 
| 10 | 9 | 3ad2ant1 1133 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 𝑂 ∈ 𝐿) | 
| 11 |  | eqid 2736 | . . . . 5
⊢
(coe1‘𝑂) = (coe1‘𝑂) | 
| 12 |  | mptcoe1matfsupp.l | . . . . 5
⊢ 𝐿 = (Base‘𝑄) | 
| 13 |  | mptcoe1matfsupp.q | . . . . 5
⊢ 𝑄 = (Poly1‘𝐴) | 
| 14 | 11, 12, 13, 4 | coe1fvalcl 22215 | . . . 4
⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) | 
| 15 | 10, 14 | sylan 580 | . . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) | 
| 16 | 2, 3, 4, 6, 8, 15 | matecld 22433 | . 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → (𝐼((coe1‘𝑂)‘𝑘)𝐽) ∈ (Base‘𝑅)) | 
| 17 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝐴) = (0g‘𝐴) | 
| 18 | 11, 12, 13, 17, 4 | coe1fsupp 22217 | . . . . . 6
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) ∈ {𝑐 ∈ ((Base‘𝐴) ↑m ℕ0)
∣ 𝑐 finSupp
(0g‘𝐴)}) | 
| 19 |  | elrabi 3686 | . . . . . 6
⊢
((coe1‘𝑂) ∈ {𝑐 ∈ ((Base‘𝐴) ↑m ℕ0)
∣ 𝑐 finSupp
(0g‘𝐴)}
→ (coe1‘𝑂) ∈ ((Base‘𝐴) ↑m
ℕ0)) | 
| 20 | 10, 18, 19 | 3syl 18 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (coe1‘𝑂) ∈ ((Base‘𝐴) ↑m
ℕ0)) | 
| 21 |  | fvex 6918 | . . . . 5
⊢
(0g‘𝐴) ∈ V | 
| 22 | 20, 21 | jctir 520 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ((coe1‘𝑂) ∈ ((Base‘𝐴) ↑m
ℕ0) ∧ (0g‘𝐴) ∈ V)) | 
| 23 | 11, 12, 13, 17 | coe1sfi 22216 | . . . . 5
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) finSupp
(0g‘𝐴)) | 
| 24 | 10, 23 | syl 17 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (coe1‘𝑂) finSupp
(0g‘𝐴)) | 
| 25 |  | fsuppmapnn0ub 14037 | . . . 4
⊢
(((coe1‘𝑂) ∈ ((Base‘𝐴) ↑m ℕ0)
∧ (0g‘𝐴) ∈ V) →
((coe1‘𝑂)
finSupp (0g‘𝐴) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) | 
| 26 | 22, 24, 25 | sylc 65 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) | 
| 27 |  | csbov 7477 | . . . . . . . . . 10
⊢
⦋𝑥 /
𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (𝐼⦋𝑥 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝐽) | 
| 28 |  | csbfv 6955 | . . . . . . . . . . 11
⊢
⦋𝑥 /
𝑘⦌((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝑥) | 
| 29 | 28 | oveqi 7445 | . . . . . . . . . 10
⊢ (𝐼⦋𝑥 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝐽) = (𝐼((coe1‘𝑂)‘𝑥)𝐽) | 
| 30 | 27, 29 | eqtri 2764 | . . . . . . . . 9
⊢
⦋𝑥 /
𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (𝐼((coe1‘𝑂)‘𝑥)𝐽) | 
| 31 | 30 | a1i 11 | . . . . . . . 8
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (𝐼((coe1‘𝑂)‘𝑥)𝐽)) | 
| 32 |  | oveq 7438 | . . . . . . . . 9
⊢
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → (𝐼((coe1‘𝑂)‘𝑥)𝐽) = (𝐼(0g‘𝐴)𝐽)) | 
| 33 | 32 | adantl 481 | . . . . . . . 8
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝐼((coe1‘𝑂)‘𝑥)𝐽) = (𝐼(0g‘𝐴)𝐽)) | 
| 34 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 35 | 2, 34 | mat0op 22426 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 36 | 35 | 3adant3 1132 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 37 | 36 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 38 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → (0g‘𝑅) = (0g‘𝑅)) | 
| 39 | 37, 38, 5, 7, 1 | ovmpod 7586 | . . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝐼(0g‘𝐴)𝐽) = (0g‘𝑅)) | 
| 40 | 39 | ad4antr 732 | . . . . . . . 8
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝐼(0g‘𝐴)𝐽) = (0g‘𝑅)) | 
| 41 | 31, 33, 40 | 3eqtrd 2780 | . . . . . . 7
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
∧ 𝑠 < 𝑥) ∧
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)) | 
| 42 | 41 | exp31 419 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑠 < 𝑥 →
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) | 
| 43 | 42 | a2d 29 | . . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((𝑠 < 𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) | 
| 44 | 43 | ralimdva 3166 | . . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) | 
| 45 | 44 | reximdva 3167 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅)))) | 
| 46 | 26, 45 | mpd 15 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌(𝐼((coe1‘𝑂)‘𝑘)𝐽) = (0g‘𝑅))) | 
| 47 | 1, 16, 46 | mptnn0fsupp 14039 | 1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ (𝐼((coe1‘𝑂)‘𝑘)𝐽)) finSupp (0g‘𝑅)) |