| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mp2pm2mp.a | . . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 2 |  | mp2pm2mp.q | . . 3
⊢ 𝑄 = (Poly1‘𝐴) | 
| 3 |  | mp2pm2mp.l | . . 3
⊢ 𝐿 = (Base‘𝑄) | 
| 4 |  | mp2pm2mp.m | . . 3
⊢  · = (
·𝑠 ‘𝑃) | 
| 5 |  | mp2pm2mp.e | . . 3
⊢ 𝐸 =
(.g‘(mulGrp‘𝑃)) | 
| 6 |  | mp2pm2mp.y | . . 3
⊢ 𝑌 = (var1‘𝑅) | 
| 7 |  | mp2pm2mp.i | . . 3
⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) | 
| 8 |  | mp2pm2mplem2.p | . . 3
⊢ 𝑃 = (Poly1‘𝑅) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | mp2pm2mplem3 22814 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))) | 
| 10 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 11 |  | eqid 2737 | . . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 12 | 8 | ply1ring 22249 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 13 | 12 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring) | 
| 14 |  | ringcmn 20279 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ CMnd) | 
| 16 | 15 | ad3antrrr 730 | . . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑃 ∈ CMnd) | 
| 17 | 16 | 3ad2ant1 1134 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ CMnd) | 
| 18 |  | simpl2 1193 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → 𝑅 ∈ Ring) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑅 ∈ Ring) | 
| 20 | 19 | 3ad2ant1 1134 | . . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) | 
| 22 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 23 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(Base‘𝐴) =
(Base‘𝐴) | 
| 24 |  | simpl2 1193 | . . . . . . . . . . . 12
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑖 ∈ 𝑁) | 
| 25 |  | simpl3 1194 | . . . . . . . . . . . 12
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ 𝑁) | 
| 26 |  | simpl3 1194 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → 𝑂 ∈ 𝐿) | 
| 27 | 26 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑂 ∈ 𝐿) | 
| 28 | 27 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿) | 
| 29 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(coe1‘𝑂) = (coe1‘𝑂) | 
| 30 | 29, 3, 2, 23 | coe1fvalcl 22214 | . . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) | 
| 31 | 28, 30 | sylan 580 | . . . . . . . . . . . 12
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) | 
| 32 | 1, 22, 23, 24, 25, 31 | matecld 22432 | . . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) | 
| 33 |  | simpr 484 | . . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 34 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) | 
| 35 | 22, 8, 6, 4, 34, 5,
10 | ply1tmcl 22275 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ0) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) | 
| 36 | 21, 32, 33, 35 | syl3anc 1373 | . . . . . . . . . 10
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) | 
| 37 | 36 | ralrimiva 3146 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ0 ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) | 
| 38 |  | simp1lr 1238 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ0) | 
| 39 |  | oveq 7437 | . . . . . . . . . . . . . . . . 17
⊢
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → (𝑖((coe1‘𝑂)‘𝑥)𝑗) = (𝑖(0g‘𝐴)𝑗)) | 
| 40 | 39 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌))) | 
| 41 |  | 3simpa 1149 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 42 | 41 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) | 
| 43 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 44 | 1, 43 | mat0op 22425 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 45 | 42, 44 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 46 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0g‘𝑅) = (0g‘𝑅)) | 
| 47 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) | 
| 48 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁) | 
| 49 |  | fvexd 6921 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0g‘𝑅) ∈ V) | 
| 50 | 45, 46, 47, 48, 49 | ovmpod 7585 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0g‘𝐴)𝑗) = (0g‘𝑅)) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → (𝑖(0g‘𝐴)𝑗) = (0g‘𝑅)) | 
| 52 | 51 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0g‘𝑅) · (𝑥𝐸𝑌))) | 
| 53 | 18 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑅 ∈ Ring) | 
| 54 | 8 | ply1sca 22254 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑅 = (Scalar‘𝑃)) | 
| 56 | 55 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) →
(0g‘𝑅) =
(0g‘(Scalar‘𝑃))) | 
| 57 | 56 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) →
((0g‘𝑅)
·
(𝑥𝐸𝑌)) =
((0g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌))) | 
| 58 | 8 | ply1lmod 22253 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) | 
| 59 | 58 | 3ad2ant2 1135 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ LMod) | 
| 60 | 59 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑃 ∈ LMod) | 
| 61 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) | 
| 62 | 8, 6, 34, 5, 10 | ply1moncl 22274 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ0)
→ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) | 
| 63 | 53, 61, 62 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → (𝑥𝐸𝑌) ∈ (Base‘𝑃)) | 
| 64 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) | 
| 65 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) | 
| 66 | 10, 64, 4, 65, 11 | lmod0vs 20893 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0g‘𝑃)) | 
| 67 | 60, 63, 66 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) →
((0g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0g‘𝑃)) | 
| 68 | 52, 57, 67 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)) | 
| 69 | 68 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) ∧ 𝑠 < 𝑥) → ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)) | 
| 70 | 40, 69 | sylan9eqr 2799 | . . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) ∧ 𝑠 < 𝑥) ∧ ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)) | 
| 71 | 70 | exp31 419 | . . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → (𝑠 < 𝑥 → (((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) | 
| 72 | 71 | a2d 29 | . . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) | 
| 73 | 72 | ralimdva 3167 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) | 
| 74 | 73 | impancom 451 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) | 
| 75 | 74 | 3impib 1117 | . . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃))) | 
| 76 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥)) | 
| 77 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → ((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝑥)) | 
| 78 | 77 | oveqd 7448 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → (𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝑥)𝑗)) | 
| 79 |  | oveq1 7438 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌)) | 
| 80 | 78, 79 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑥 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌))) | 
| 81 | 80 | eqeq1d 2739 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃) ↔ ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃))) | 
| 82 | 76, 81 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) | 
| 83 | 82 | cbvralvw 3237 | . . . . . . . . . 10
⊢
(∀𝑘 ∈
ℕ0 (𝑠 <
𝑘 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃)) ↔ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃))) | 
| 84 | 75, 83 | sylibr 234 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃))) | 
| 85 | 10, 11, 17, 37, 38, 84 | gsummptnn0fz 20004 | . . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) | 
| 86 | 85 | fveq2d 6910 | . . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) | 
| 87 | 86 | fveq1d 6908 | . . . . . 6
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = ((coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) | 
| 88 |  | simpllr 776 | . . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝐾 ∈
ℕ0) | 
| 89 | 88 | 3ad2ant1 1134 | . . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈
ℕ0) | 
| 90 | 36 | expcom 413 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))) | 
| 91 |  | elfznn0 13660 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ0) | 
| 92 | 90, 91 | syl11 33 | . . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))) | 
| 93 | 92 | ralrimiv 3145 | . . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) | 
| 94 |  | fzfid 14014 | . . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin) | 
| 95 | 8, 10, 20, 89, 93, 94 | coe1fzgsumd 22308 | . . . . . 6
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) | 
| 96 | 87, 95 | eqtrd 2777 | . . . . 5
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) | 
| 97 | 96 | mpoeq3dva 7510 | . . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))) | 
| 98 | 18 | 3ad2ant1 1134 | . . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 99 | 98 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring) | 
| 100 |  | simpl2 1193 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑖 ∈ 𝑁) | 
| 101 |  | simpl3 1194 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑗 ∈ 𝑁) | 
| 102 | 26 | 3ad2ant1 1134 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿) | 
| 103 | 102, 91, 30 | syl2an 596 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) | 
| 104 | 1, 22, 23, 100, 101, 103 | matecld 22432 | . . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) | 
| 105 | 91 | adantl 481 | . . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ0) | 
| 106 | 43, 22, 8, 6, 4, 34,
5 | coe1tm 22276 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ0) →
(coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) | 
| 107 | 99, 104, 105, 106 | syl3anc 1373 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) | 
| 108 |  | eqeq1 2741 | . . . . . . . . . . 11
⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘)) | 
| 109 | 108 | ifbid 4549 | . . . . . . . . . 10
⊢ (𝑙 = 𝐾 → if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) | 
| 110 | 109 | adantl 481 | . . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑙 = 𝐾) → if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) | 
| 111 |  | simpl1r 1226 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝐾 ∈
ℕ0) | 
| 112 |  | ovex 7464 | . . . . . . . . . . 11
⊢ (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ V | 
| 113 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V | 
| 114 | 112, 113 | ifex 4576 | . . . . . . . . . 10
⊢ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) ∈ V | 
| 115 | 114 | a1i 11 | . . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) ∈ V) | 
| 116 | 107, 110,
111, 115 | fvmptd 7023 | . . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) | 
| 117 | 116 | mpteq2dva 5242 | . . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) | 
| 118 | 117 | oveq2d 7447 | . . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) | 
| 119 | 118 | mpoeq3dva 7510 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))))) | 
| 120 | 119 | ad2antrr 726 | . . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))))) | 
| 121 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾)) | 
| 122 |  | fveqeq2 6915 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐾 → (((coe1‘𝑂)‘𝑥) = (0g‘𝐴) ↔ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴))) | 
| 123 | 121, 122 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)))) | 
| 124 | 123 | rspcva 3620 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴))) | 
| 125 | 1, 43 | mat0op 22425 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 126 | 125 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)) = (0g‘𝐴)) | 
| 127 | 126 | 3adant3 1133 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)) = (0g‘𝐴)) | 
| 128 | 127 | ad3antlr 731 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)) = (0g‘𝐴)) | 
| 129 |  | elfz2nn0 13658 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝑘 ≤ 𝑠)) | 
| 130 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) | 
| 131 | 130 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑘 ∈
ℝ) | 
| 132 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑠 ∈ ℕ0
→ 𝑠 ∈
ℝ) | 
| 133 | 132 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑠 ∈
ℝ) | 
| 134 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) | 
| 135 | 134 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℝ) | 
| 136 |  | lelttr 11351 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾)) | 
| 137 | 131, 133,
135, 136 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾)) | 
| 138 |  | animorr 981 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)) | 
| 139 |  | df-ne 2941 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘) | 
| 140 | 130 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → 𝑘 ∈ ℝ) | 
| 141 |  | lttri2 11343 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) | 
| 142 | 134, 140,
141 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) | 
| 143 | 142 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) | 
| 144 | 139, 143 | bitr3id 285 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → (¬ 𝐾 = 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) | 
| 145 | 138, 144 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → ¬ 𝐾 = 𝑘) | 
| 146 | 145 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑘 < 𝐾 → ¬ 𝐾 = 𝑘)) | 
| 147 | 137, 146 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → ¬ 𝐾 = 𝑘)) | 
| 148 | 147 | exp4b 430 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐾 ∈ ℕ0 → (𝑘 ≤ 𝑠 → (𝑠 < 𝐾 → ¬ 𝐾 = 𝑘)))) | 
| 149 | 148 | com24 95 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝑠 < 𝐾 → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘)))) | 
| 150 | 149 | expimpd 453 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 ∈ ℕ0
→ ((𝑠 ∈
ℕ0 ∧ 𝑠
< 𝐾) → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘)))) | 
| 151 | 150 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ ℕ0
→ (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘)))) | 
| 152 | 151 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘))) | 
| 153 | 152 | 3adant2 1132 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0 ∧ 𝑘
≤ 𝑠) → ((𝑠 ∈ ℕ0
∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘))) | 
| 154 | 129, 153 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘))) | 
| 155 | 154 | com13 88 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐾 ∈ ℕ0
→ ((𝑠 ∈
ℕ0 ∧ 𝑠
< 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))) | 
| 156 | 155 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))) | 
| 157 | 156 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)) | 
| 159 | 158 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)) | 
| 160 | 159 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐾 = 𝑘) | 
| 161 | 160 | iffalsed 4536 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = (0g‘𝑅)) | 
| 162 | 161 | mpteq2dva 5242 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) | 
| 163 | 162 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅)))) | 
| 164 |  | ringmnd 20240 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 165 | 164 | 3ad2ant2 1135 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd) | 
| 166 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0...𝑠) ∈
V | 
| 167 | 43 | gsumz 18849 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
(0g‘𝑅))) =
(0g‘𝑅)) | 
| 168 | 165, 166,
167 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) = (0g‘𝑅)) | 
| 169 | 168 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) = (0g‘𝑅)) | 
| 170 | 169 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) = (0g‘𝑅)) | 
| 171 | 163, 170 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) = (0g‘𝑅)) | 
| 172 | 171 | mpoeq3dva 7510 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) | 
| 173 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) | 
| 174 | 128, 172,
173 | 3eqtr4d 2787 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)) | 
| 175 | 174 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) → (((coe1‘𝑂)‘𝐾) = (0g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) | 
| 176 | 175 | expr 456 | . . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ0) → (𝑠 < 𝐾 → (((coe1‘𝑂)‘𝐾) = (0g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))) | 
| 177 | 176 | a2d 29 | . . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ0) → ((𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))) | 
| 178 | 177 | exp31 419 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ ((𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → ((𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) | 
| 179 | 178 | com14 96 | . . . . . . . . . . . 12
⊢ ((𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → (𝐾 ∈ ℕ0
→ (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) | 
| 180 | 124, 179 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → (𝐾 ∈ ℕ0
→ (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) | 
| 181 | 180 | ex 412 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → (𝐾 ∈ ℕ0
→ (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))))))) | 
| 182 | 181 | com25 99 | . . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))))))) | 
| 183 | 182 | pm2.43i 52 | . . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ ((𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) | 
| 184 | 183 | impcom 407 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑠 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))))) | 
| 185 | 184 | imp31 417 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) | 
| 186 | 185 | com12 32 | . . . . 5
⊢ (𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) | 
| 187 | 165 | ad3antrrr 730 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑅 ∈ Mnd) | 
| 188 | 187 | adantl 481 | . . . . . . . . . 10
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → 𝑅 ∈ Mnd) | 
| 189 | 188 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Mnd) | 
| 190 |  | ovexd 7466 | . . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V) | 
| 191 |  | lenlt 11339 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾)) | 
| 192 | 134, 132,
191 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾)) | 
| 193 |  | simpll 767 | . . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈
ℕ0) | 
| 194 |  | simplr 769 | . . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ0) | 
| 195 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠) | 
| 196 |  | elfz2nn0 13658 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (0...𝑠) ↔ (𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝐾 ≤ 𝑠)) | 
| 197 | 193, 194,
195, 196 | syl3anbrc 1344 | . . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ (0...𝑠)) | 
| 198 | 197 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐾 ≤ 𝑠 → 𝐾 ∈ (0...𝑠))) | 
| 199 | 192, 198 | sylbird 260 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠))) | 
| 200 | 199 | ad4ant23 753 | . . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠))) | 
| 201 | 200 | impcom 407 | . . . . . . . . . 10
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → 𝐾 ∈ (0...𝑠)) | 
| 202 | 201 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ (0...𝑠)) | 
| 203 |  | eqcom 2744 | . . . . . . . . . . 11
⊢ (𝐾 = 𝑘 ↔ 𝑘 = 𝐾) | 
| 204 |  | ifbi 4548 | . . . . . . . . . . 11
⊢ ((𝐾 = 𝑘 ↔ 𝑘 = 𝐾) → if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝑘 = 𝐾, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) | 
| 205 | 203, 204 | ax-mp 5 | . . . . . . . . . 10
⊢ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝑘 = 𝐾, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) | 
| 206 | 205 | mpteq2i 5247 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐾, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) | 
| 207 |  | simpl2 1193 | . . . . . . . . . . . 12
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑖 ∈ 𝑁) | 
| 208 |  | simpl3 1194 | . . . . . . . . . . . 12
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ 𝑁) | 
| 209 | 27 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → 𝑂 ∈ 𝐿) | 
| 210 | 209 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿) | 
| 211 | 210, 30 | sylan 580 | . . . . . . . . . . . 12
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) | 
| 212 | 1, 22, 23, 207, 208, 211 | matecld 22432 | . . . . . . . . . . 11
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) | 
| 213 | 91, 212 | sylan2 593 | . . . . . . . . . 10
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) | 
| 214 | 213 | ralrimiva 3146 | . . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) | 
| 215 | 43, 189, 190, 202, 206, 214 | gsummpt1n0 19983 | . . . . . . . 8
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) = ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) | 
| 216 | 215 | mpoeq3dva 7510 | . . . . . . 7
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))) | 
| 217 |  | csbov 7476 | . . . . . . . . . . . . . . 15
⊢
⦋𝐾 /
𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝑗) | 
| 218 |  | csbfv 6956 | . . . . . . . . . . . . . . . . 17
⊢
⦋𝐾 /
𝑘⦌((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝐾) | 
| 219 | 218 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ ⦋𝐾 /
𝑘⦌((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝐾)) | 
| 220 | 219 | oveqd 7448 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ (𝑖⦋𝐾 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗)) | 
| 221 | 217, 220 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ ⦋𝐾 /
𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗)) | 
| 222 | 221 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗)) | 
| 223 | 222 | mpoeq3dv 7512 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe1‘𝑂)‘𝐾)𝑗))) | 
| 224 |  | oveq12 7440 | . . . . . . . . . . . . 13
⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖((coe1‘𝑂)‘𝐾)𝑗) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) | 
| 225 | 224 | adantl 481 | . . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (𝑖((coe1‘𝑂)‘𝐾)𝑗) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) | 
| 226 |  | simprl 771 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁) | 
| 227 |  | simprr 773 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁) | 
| 228 |  | ovexd 7466 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe1‘𝑂)‘𝐾)𝑏) ∈ V) | 
| 229 | 223, 225,
226, 227, 228 | ovmpod 7585 | . . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) | 
| 230 | 229 | ralrimivva 3202 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) | 
| 231 |  | simpl1 1192 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ Fin) | 
| 232 | 218 | oveqi 7444 | . . . . . . . . . . . . . 14
⊢ (𝑖⦋𝐾 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗) | 
| 233 | 217, 232 | eqtri 2765 | . . . . . . . . . . . . 13
⊢
⦋𝐾 /
𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗) | 
| 234 |  | simp2 1138 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 235 |  | simp3 1139 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) | 
| 236 | 29, 3, 2, 23 | coe1fvalcl 22214 | . . . . . . . . . . . . . . . 16
⊢ ((𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ0) →
((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) | 
| 237 | 236 | 3ad2antl3 1188 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) | 
| 238 | 237 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) | 
| 239 | 1, 22, 23, 234, 235, 238 | matecld 22432 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe1‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅)) | 
| 240 | 233, 239 | eqeltrid 2845 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) | 
| 241 | 1, 22, 23, 231, 18, 240 | matbas2d 22429 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴)) | 
| 242 | 1, 23 | eqmat 22430 | . . . . . . . . . . 11
⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴) ∧ ((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏))) | 
| 243 | 241, 237,
242 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏))) | 
| 244 | 230, 243 | mpbird 257 | . . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾)) | 
| 245 | 244 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾)) | 
| 246 | 245 | adantl 481 | . . . . . . 7
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾)) | 
| 247 | 216, 246 | eqtrd 2777 | . . . . . 6
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)) | 
| 248 | 247 | ex 412 | . . . . 5
⊢ (¬
𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) | 
| 249 | 186, 248 | pm2.61i 182 | . . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)) | 
| 250 | 97, 120, 249 | 3eqtrd 2781 | . . 3
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe1‘𝑂)‘𝐾)) | 
| 251 |  | eqid 2737 | . . . . . 6
⊢
(0g‘𝐴) = (0g‘𝐴) | 
| 252 | 29, 3, 2, 251 | coe1sfi 22215 | . . . . 5
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) finSupp
(0g‘𝐴)) | 
| 253 | 26, 252 | syl 17 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
(coe1‘𝑂)
finSupp (0g‘𝐴)) | 
| 254 | 29, 3, 2, 251, 23 | coe1fsupp 22216 | . . . . . 6
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑m ℕ0)
∣ 𝑥 finSupp
(0g‘𝐴)}) | 
| 255 |  | elrabi 3687 | . . . . . 6
⊢
((coe1‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑m ℕ0)
∣ 𝑥 finSupp
(0g‘𝐴)}
→ (coe1‘𝑂) ∈ ((Base‘𝐴) ↑m
ℕ0)) | 
| 256 | 26, 254, 255 | 3syl 18 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
(coe1‘𝑂)
∈ ((Base‘𝐴)
↑m ℕ0)) | 
| 257 |  | fvex 6919 | . . . . 5
⊢
(0g‘𝐴) ∈ V | 
| 258 |  | fsuppmapnn0ub 14036 | . . . . 5
⊢
(((coe1‘𝑂) ∈ ((Base‘𝐴) ↑m ℕ0)
∧ (0g‘𝐴) ∈ V) →
((coe1‘𝑂)
finSupp (0g‘𝐴) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) | 
| 259 | 256, 257,
258 | sylancl 586 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
((coe1‘𝑂)
finSupp (0g‘𝐴) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) | 
| 260 | 253, 259 | mpd 15 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) | 
| 261 | 250, 260 | r19.29a 3162 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe1‘𝑂)‘𝐾)) | 
| 262 | 9, 261 | eqtrd 2777 | 1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe1‘𝑂)‘𝐾)) |