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 20432 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))) |
10 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑃) |
11 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) |
12 | 8 | ply1ring 19439 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
13 | 12 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ Ring) |
14 | | ringcmn 18404 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ CMnd) |
16 | 15 | ad3antrrr 762 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑃 ∈ CMnd) |
17 | 16 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ CMnd) |
18 | | simpl2 1058 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → 𝑅 ∈ Ring) |
19 | 18 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑅 ∈ Ring) |
20 | 19 | 3ad2ant1 1075 |
. . . . . . . . . . . 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 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
23 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝐴) =
(Base‘𝐴) |
24 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑖 ∈ 𝑁) |
25 | | simpl3 1059 |
. . . . . . . . . . . 12
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ 𝑁) |
26 | | simpl3 1059 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → 𝑂 ∈ 𝐿) |
27 | 26 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑂 ∈ 𝐿) |
28 | 27 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿) |
29 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(coe1‘𝑂) = (coe1‘𝑂) |
30 | 29, 3, 2, 23 | coe1fvalcl 19403 |
. . . . . . . . . . . . 13
⊢ ((𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) |
31 | 28, 30 | sylan 487 |
. . . . . . . . . . . 12
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) |
32 | 1, 22, 23, 24, 25, 31 | matecld 20051 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) |
33 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
34 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
35 | 22, 8, 6, 4, 34, 5,
10 | ply1tmcl 19463 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ0) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) |
36 | 21, 32, 33, 35 | syl3anc 1318 |
. . . . . . . . . 10
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) |
37 | 36 | ralrimiva 2949 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ0 ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) |
38 | | simp1lr 1118 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑠 ∈ ℕ0) |
39 | | oveq 6555 |
. . . . . . . . . . . . . . . . 17
⊢
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → (𝑖((coe1‘𝑂)‘𝑥)𝑗) = (𝑖(0g‘𝐴)𝑗)) |
40 | 39 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢
(((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌))) |
41 | | 3simpa 1051 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
42 | 41 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
43 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0g‘𝑅) = (0g‘𝑅) |
44 | 1, 43 | mat0op 20044 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0g‘𝑅))) |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0g‘𝐴) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (0g‘𝑅))) |
46 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 = 𝑖 ∧ 𝑏 = 𝑗)) → (0g‘𝑅) = (0g‘𝑅)) |
47 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
48 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁) |
49 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0g‘𝑅) ∈ V |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0g‘𝑅) ∈ V) |
51 | 45, 46, 47, 48, 50 | ovmpt2d 6686 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(0g‘𝐴)𝑗) = (0g‘𝑅)) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → (𝑖(0g‘𝐴)𝑗) = (0g‘𝑅)) |
53 | 52 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = ((0g‘𝑅) · (𝑥𝐸𝑌))) |
54 | 18 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑅 ∈ Ring) |
55 | 8 | ply1sca 19444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑅 = (Scalar‘𝑃)) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) →
(0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
58 | 57 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) →
((0g‘𝑅)
·
(𝑥𝐸𝑌)) =
((0g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌))) |
59 | 8 | ply1lmod 19443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
60 | 59 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑃 ∈ LMod) |
61 | 60 | ad4antr 764 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑃 ∈ LMod) |
62 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
63 | 8, 6, 34, 5, 10 | ply1moncl 19462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℕ0)
→ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) |
64 | 54, 62, 63 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → (𝑥𝐸𝑌) ∈ (Base‘𝑃)) |
65 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
66 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
67 | 10, 65, 4, 66, 11 | lmod0vs 18719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ LMod ∧ (𝑥𝐸𝑌) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0g‘𝑃)) |
68 | 61, 64, 67 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) →
((0g‘(Scalar‘𝑃)) · (𝑥𝐸𝑌)) = (0g‘𝑃)) |
69 | 53, 58, 68 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) ∧ 𝑠 < 𝑥) → ((𝑖(0g‘𝐴)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)) |
71 | 40, 70 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) ∧ 𝑠 < 𝑥) ∧ ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)) |
72 | 71 | exp31 628 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → (𝑠 < 𝑥 → (((coe1‘𝑂)‘𝑥) = (0g‘𝐴) → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) |
73 | 72 | a2d 29 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) |
74 | 73 | ralimdva 2945 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) |
75 | 74 | impancom 455 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) |
76 | 75 | 3impib 1254 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃))) |
77 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (𝑠 < 𝑘 ↔ 𝑠 < 𝑥)) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑥 → ((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝑥)) |
79 | 78 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → (𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝑥)𝑗)) |
80 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑥 → (𝑘𝐸𝑌) = (𝑥𝐸𝑌)) |
81 | 79, 80 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑥 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌))) |
82 | 81 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃) ↔ ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃))) |
83 | 77, 82 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → ((𝑠 < 𝑘 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃)) ↔ (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃)))) |
84 | 83 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
ℕ0 (𝑠 <
𝑘 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃)) ↔ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑖((coe1‘𝑂)‘𝑥)𝑗) · (𝑥𝐸𝑌)) = (0g‘𝑃))) |
85 | 76, 84 | sylibr 223 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = (0g‘𝑃))) |
86 | 10, 11, 17, 37, 38, 85 | gsummptnn0fzv 18206 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σg (𝑘 ∈ ℕ0
↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) |
87 | 86 | fveq2d 6107 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) |
88 | 87 | fveq1d 6105 |
. . . . . 6
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = ((coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) |
89 | | simpllr 795 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝐾 ∈
ℕ0) |
90 | 89 | 3ad2ant1 1075 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈
ℕ0) |
91 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ0) |
92 | 36 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))) |
93 | 91, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑠) → ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))) |
94 | 93 | com12 32 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃))) |
95 | 94 | ralrimiv 2948 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)) ∈ (Base‘𝑃)) |
96 | | fzfid 12634 |
. . . . . . 7
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ Fin) |
97 | 8, 10, 20, 90, 95, 96 | coe1fzgsumd 19493 |
. . . . . 6
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑃 Σg
(𝑘 ∈ (0...𝑠) ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) |
98 | 88, 97 | eqtrd 2644 |
. . . . 5
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) |
99 | 98 | mpt2eq3dva 6617 |
. . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))))) |
100 | 18 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
101 | 100 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring) |
102 | | simpl2 1058 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑖 ∈ 𝑁) |
103 | | simpl3 1059 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑗 ∈ 𝑁) |
104 | 26 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿) |
105 | 104, 91, 30 | syl2an 493 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) |
106 | 1, 22, 23, 102, 103, 105 | matecld 20051 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) |
107 | 91 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ0) |
108 | 43, 22, 8, 6, 4, 34,
5 | coe1tm 19464 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅) ∧ 𝑘 ∈ ℕ0) →
(coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) |
109 | 101, 106,
107, 108 | syl3anc 1318 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) |
110 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝐾 → (𝑙 = 𝑘 ↔ 𝐾 = 𝑘)) |
111 | 110 | ifbid 4058 |
. . . . . . . . . 10
⊢ (𝑙 = 𝐾 → if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) |
112 | 111 | adantl 481 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑙 = 𝐾) → if(𝑙 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) |
113 | | simpl1r 1106 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → 𝐾 ∈
ℕ0) |
114 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ V |
115 | 114, 49 | ifex 4106 |
. . . . . . . . . 10
⊢ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) ∈ V |
116 | 115 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) ∈ V) |
117 | 109, 112,
113, 116 | fvmptd 6197 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾) = if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) |
118 | 117 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) |
119 | 118 | oveq2d 6565 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) |
120 | 119 | mpt2eq3dva 6617 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))))) |
121 | 120 | ad2antrr 758 |
. . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))‘𝐾)))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))))) |
122 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐾 → (𝑠 < 𝑥 ↔ 𝑠 < 𝐾)) |
123 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐾 → ((coe1‘𝑂)‘𝑥) = ((coe1‘𝑂)‘𝐾)) |
124 | 123 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐾 → (((coe1‘𝑂)‘𝑥) = (0g‘𝐴) ↔ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴))) |
125 | 122, 124 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐾 → ((𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) ↔ (𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)))) |
126 | 125 | rspcva 3280 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴))) |
127 | 1, 43 | mat0op 20044 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
128 | 127 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)) = (0g‘𝐴)) |
129 | 128 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)) = (0g‘𝐴)) |
130 | 129 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅)) = (0g‘𝐴)) |
131 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝑘 ≤ 𝑠)) |
132 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
133 | 132 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑘 ∈
ℝ) |
134 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑠 ∈ ℕ0
→ 𝑠 ∈
ℝ) |
135 | 134 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑠 ∈
ℝ) |
136 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
137 | 136 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℝ) |
138 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾)) |
139 | 133, 135,
137, 138 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → 𝑘 < 𝐾)) |
140 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → 𝑘 < 𝐾) |
141 | 140 | olcd 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → (𝐾 < 𝑘 ∨ 𝑘 < 𝐾)) |
142 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐾 ≠ 𝑘 ↔ ¬ 𝐾 = 𝑘) |
143 | 132 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → 𝑘 ∈ ℝ) |
144 | | lttri2 9999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐾 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) |
145 | 136, 143,
144 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) |
146 | 145 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → (𝐾 ≠ 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) |
147 | 142, 146 | syl5bbr 273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → (¬ 𝐾 = 𝑘 ↔ (𝐾 < 𝑘 ∨ 𝑘 < 𝐾))) |
148 | 141, 147 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ 𝑘 < 𝐾) → ¬ 𝐾 = 𝑘) |
149 | 148 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑘 < 𝐾 → ¬ 𝐾 = 𝑘)) |
150 | 139, 149 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐾) → ¬ 𝐾 = 𝑘)) |
151 | 150 | exp4b 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐾 ∈ ℕ0 → (𝑘 ≤ 𝑠 → (𝑠 < 𝐾 → ¬ 𝐾 = 𝑘)))) |
152 | 151 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝑠 < 𝐾 → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘)))) |
153 | 152 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑘 ∈ ℕ0
→ ((𝑠 ∈
ℕ0 ∧ 𝑠
< 𝐾) → (𝑘 ≤ 𝑠 → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘)))) |
154 | 153 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ ℕ0
→ (𝑘 ≤ 𝑠 → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘)))) |
155 | 154 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 ≤ 𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘))) |
156 | 155 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑘 ∈ ℕ0
∧ 𝑠 ∈
ℕ0 ∧ 𝑘
≤ 𝑠) → ((𝑠 ∈ ℕ0
∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘))) |
157 | 131, 156 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝐾 ∈ ℕ0 → ¬
𝐾 = 𝑘))) |
158 | 157 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐾 ∈ ℕ0
→ ((𝑠 ∈
ℕ0 ∧ 𝑠
< 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))) |
159 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) → ((𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘))) |
160 | 159 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)) |
161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)) |
162 | 161 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) → ¬ 𝐾 = 𝑘)) |
163 | 162 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐾 = 𝑘) |
164 | 163 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = (0g‘𝑅)) |
165 | 164 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) |
166 | 165 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅)))) |
167 | | ringmnd 18379 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
168 | 167 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑅 ∈ Mnd) |
169 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0...𝑠) ∈
V |
170 | 43 | gsumz 17197 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
171 | 168, 169,
170 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) = (0g‘𝑅)) |
172 | 171 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) = (0g‘𝑅)) |
173 | 172 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (0g‘𝑅))) = (0g‘𝑅)) |
174 | 166, 173 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) = (0g‘𝑅)) |
175 | 174 | mpt2eq3dva 6617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
176 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) |
177 | 130, 175,
176 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) ∧ ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)) |
178 | 177 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ (𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐾)) → (((coe1‘𝑂)‘𝐾) = (0g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) |
179 | 178 | expr 641 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ0) → (𝑠 < 𝐾 → (((coe1‘𝑂)‘𝐾) = (0g‘𝐴) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))) |
180 | 179 | a2d 29 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ ℕ0
∧ (𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿)) ∧ 𝑠 ∈ ℕ0) → ((𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))) |
181 | 180 | exp31 628 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ ((𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → ((𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) |
182 | 181 | com14 94 |
. . . . . . . . . . . 12
⊢ ((𝑠 < 𝐾 → ((coe1‘𝑂)‘𝐾) = (0g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → (𝐾 ∈ ℕ0
→ (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) |
183 | 126, 182 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → (𝐾 ∈ ℕ0
→ (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) |
184 | 183 | ex 449 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 → (𝐾 ∈ ℕ0
→ (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))))))) |
185 | 184 | com25 97 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))))))) |
186 | 185 | pm2.43i 50 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ ((𝑁 ∈ Fin ∧
𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑠 ∈ ℕ0 →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)))))) |
187 | 186 | impcom 445 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑠 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))))) |
188 | 187 | imp31 447 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑠 < 𝐾 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) |
189 | 188 | com12 32 |
. . . . 5
⊢ (𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) |
190 | 168 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → 𝑅 ∈ Mnd) |
191 | 190 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → 𝑅 ∈ Mnd) |
192 | 191 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Mnd) |
193 | 169 | a1i 11 |
. . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (0...𝑠) ∈ V) |
194 | | lenlt 9995 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾)) |
195 | 136, 134,
194 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐾 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐾)) |
196 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈
ℕ0) |
197 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝑠 ∈ ℕ0) |
198 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝐾 ≤ 𝑠) |
199 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ (0...𝑠) ↔ (𝐾 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0
∧ 𝐾 ≤ 𝑠)) |
200 | 196, 197,
198, 199 | syl3anbrc 1239 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) ∧ 𝐾 ≤ 𝑠) → 𝐾 ∈ (0...𝑠)) |
201 | 200 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (𝐾 ≤ 𝑠 → 𝐾 ∈ (0...𝑠))) |
202 | 195, 201 | sylbird 249 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ 𝑠 ∈
ℕ0) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠))) |
203 | 202 | adantll 746 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
→ (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠))) |
204 | 203 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (¬ 𝑠 < 𝐾 → 𝐾 ∈ (0...𝑠))) |
205 | 204 | impcom 445 |
. . . . . . . . . 10
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → 𝐾 ∈ (0...𝑠)) |
206 | 205 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐾 ∈ (0...𝑠)) |
207 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (𝐾 = 𝑘 ↔ 𝑘 = 𝐾) |
208 | | ifbi 4057 |
. . . . . . . . . . 11
⊢ ((𝐾 = 𝑘 ↔ 𝑘 = 𝐾) → if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝑘 = 𝐾, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) |
209 | 207, 208 | ax-mp 5 |
. . . . . . . . . 10
⊢ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) = if(𝑘 = 𝐾, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)) |
210 | 209 | mpteq2i 4669 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐾, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))) |
211 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑖 ∈ 𝑁) |
212 | | simpl3 1059 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ 𝑁) |
213 | 27 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → 𝑂 ∈ 𝐿) |
214 | 213 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑂 ∈ 𝐿) |
215 | 214, 30 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝑂)‘𝑘) ∈ (Base‘𝐴)) |
216 | 1, 22, 23, 211, 212, 215 | matecld 20051 |
. . . . . . . . . . 11
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ ℕ0) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) |
217 | 91, 216 | sylan2 490 |
. . . . . . . . . 10
⊢ ((((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑘 ∈ (0...𝑠)) → (𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) |
218 | 217 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ∀𝑘 ∈ (0...𝑠)(𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) |
219 | 43, 192, 193, 206, 210, 218 | gsummpt1n0 18187 |
. . . . . . . 8
⊢ (((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅)))) = ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) |
220 | 219 | mpt2eq3dva 6617 |
. . . . . . 7
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))) |
221 | | csbov 6586 |
. . . . . . . . . . . . . . 15
⊢
⦋𝐾 /
𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖⦋𝐾 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝑗) |
222 | | csbfv 6143 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝐾 /
𝑘⦌((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝐾) |
223 | 222 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ ⦋𝐾 /
𝑘⦌((coe1‘𝑂)‘𝑘) = ((coe1‘𝑂)‘𝐾)) |
224 | 223 | oveqd 6566 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ (𝑖⦋𝐾 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗)) |
225 | 221, 224 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ ⦋𝐾 /
𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗)) |
226 | 225 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗)) |
227 | 226 | mpt2eq3dv 6619 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖((coe1‘𝑂)‘𝐾)𝑗))) |
228 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → (𝑖((coe1‘𝑂)‘𝐾)𝑗) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) |
229 | 228 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) ∧ (𝑖 = 𝑎 ∧ 𝑗 = 𝑏)) → (𝑖((coe1‘𝑂)‘𝐾)𝑗) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) |
230 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑎 ∈ 𝑁) |
231 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → 𝑏 ∈ 𝑁) |
232 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑎((coe1‘𝑂)‘𝐾)𝑏) ∈ V |
233 | 232 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎((coe1‘𝑂)‘𝐾)𝑏) ∈ V) |
234 | 227, 229,
230, 231, 233 | ovmpt2d 6686 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) |
235 | 234 | ralrimivva 2954 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏)) |
236 | | simpl1 1057 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ Fin) |
237 | 222 | oveqi 6562 |
. . . . . . . . . . . . . 14
⊢ (𝑖⦋𝐾 / 𝑘⦌((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗) |
238 | 221, 237 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢
⦋𝐾 /
𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) = (𝑖((coe1‘𝑂)‘𝐾)𝑗) |
239 | | simp2 1055 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
240 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
241 | 29, 3, 2, 23 | coe1fvalcl 19403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑂 ∈ 𝐿 ∧ 𝐾 ∈ ℕ0) →
((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) |
242 | 241 | 3ad2antl3 1218 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) |
243 | 242 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) |
244 | 1, 22, 23, 239, 240, 243 | matecld 20051 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖((coe1‘𝑂)‘𝐾)𝑗) ∈ (Base‘𝑅)) |
245 | 238, 244 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗) ∈ (Base‘𝑅)) |
246 | 1, 22, 23, 236, 18, 245 | matbas2d 20048 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴)) |
247 | 1, 23 | eqmat 20049 |
. . . . . . . . . . 11
⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) ∈ (Base‘𝐴) ∧ ((coe1‘𝑂)‘𝐾) ∈ (Base‘𝐴)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏))) |
248 | 246, 242,
247 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾) ↔ ∀𝑎 ∈ 𝑁 ∀𝑏 ∈ 𝑁 (𝑎(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗))𝑏) = (𝑎((coe1‘𝑂)‘𝐾)𝑏))) |
249 | 235, 248 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾)) |
250 | 249 | ad2antrr 758 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾)) |
251 | 250 | adantl 481 |
. . . . . . 7
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ⦋𝐾 / 𝑘⦌(𝑖((coe1‘𝑂)‘𝑘)𝑗)) = ((coe1‘𝑂)‘𝐾)) |
252 | 220, 251 | eqtrd 2644 |
. . . . . 6
⊢ ((¬
𝑠 < 𝐾 ∧ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)) |
253 | 252 | ex 449 |
. . . . 5
⊢ (¬
𝑠 < 𝐾 → (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾))) |
254 | 189, 253 | pm2.61i 175 |
. . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐾 = 𝑘, (𝑖((coe1‘𝑂)‘𝑘)𝑗), (0g‘𝑅))))) = ((coe1‘𝑂)‘𝐾)) |
255 | 99, 121, 254 | 3eqtrd 2648 |
. . 3
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) ∧ 𝑠 ∈ ℕ0)
∧ ∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe1‘𝑂)‘𝐾)) |
256 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐴) = (0g‘𝐴) |
257 | 29, 3, 2, 256 | coe1sfi 19404 |
. . . . 5
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) finSupp
(0g‘𝐴)) |
258 | 26, 257 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
(coe1‘𝑂)
finSupp (0g‘𝐴)) |
259 | 29, 3, 2, 256, 23 | coe1fsupp 19405 |
. . . . . 6
⊢ (𝑂 ∈ 𝐿 → (coe1‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∣ 𝑥 finSupp (0g‘𝐴)}) |
260 | | elrabi 3328 |
. . . . . 6
⊢
((coe1‘𝑂) ∈ {𝑥 ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∣ 𝑥 finSupp (0g‘𝐴)} →
(coe1‘𝑂)
∈ ((Base‘𝐴)
↑𝑚 ℕ0)) |
261 | 26, 259, 260 | 3syl 18 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
(coe1‘𝑂)
∈ ((Base‘𝐴)
↑𝑚 ℕ0)) |
262 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐴) ∈ V |
263 | | fsuppmapnn0ub 12657 |
. . . . 5
⊢
(((coe1‘𝑂) ∈ ((Base‘𝐴) ↑𝑚
ℕ0) ∧ (0g‘𝐴) ∈ V) →
((coe1‘𝑂)
finSupp (0g‘𝐴) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) |
264 | 261, 262,
263 | sylancl 693 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
((coe1‘𝑂)
finSupp (0g‘𝐴) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴)))) |
265 | 258, 264 | mpd 15 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) →
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((coe1‘𝑂)‘𝑥) = (0g‘𝐴))) |
266 | 255, 265 | r19.29a 3060 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg
(𝑘 ∈
ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾)) = ((coe1‘𝑂)‘𝐾)) |
267 | 9, 266 | eqtrd 2644 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe1‘𝑂)‘𝐾)) |