Step | Hyp | Ref
| Expression |
1 | | m2cpminvid2lem.s |
. . . . . . . 8
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
2 | | m2cpminvid2lem.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃) |
4 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(𝑁 Mat
𝑃)) = (Base‘(𝑁 Mat 𝑃)) |
5 | 1, 2, 3, 4 | cpmatelimp 20517 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)))) |
6 | 5 | 3impia 1261 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))) |
7 | | simpr 477 |
. . . . . 6
⊢ ((𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)) |
9 | 8 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)) |
10 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑖𝑀𝑗) = (𝑥𝑀𝑗)) |
11 | 10 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑥𝑀𝑗))) |
12 | 11 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑘) = ((coe1‘(𝑥𝑀𝑗))‘𝑘)) |
13 | 12 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑖 = 𝑥 → (((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅))) |
14 | 13 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑖 = 𝑥 → (∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅))) |
15 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑦 → (𝑥𝑀𝑗) = (𝑥𝑀𝑦)) |
16 | 15 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → (coe1‘(𝑥𝑀𝑗)) = (coe1‘(𝑥𝑀𝑦))) |
17 | 16 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((coe1‘(𝑥𝑀𝑗))‘𝑘) = ((coe1‘(𝑥𝑀𝑦))‘𝑘)) |
18 | 17 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑗 = 𝑦 → (((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
19 | 18 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑗 = 𝑦 → (∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
20 | 14, 19 | rspc2v 3322 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) → ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
21 | 20 | adantl 482 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) → ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
22 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((coe1‘(𝑥𝑀𝑦))‘𝑘) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
23 | 22 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅) ↔ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅))) |
24 | 23 | cbvralv 3171 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅) ↔ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) |
25 | | simpl2 1065 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑅 ∈ Ring) |
26 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑃) =
(Base‘𝑃) |
27 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑥 ∈ 𝑁) |
28 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑦 ∈ 𝑁) |
30 | 1, 2, 3, 4 | cpmatpmat 20515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ (Base‘(𝑁 Mat 𝑃))) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑀 ∈ (Base‘(𝑁 Mat 𝑃))) |
32 | 3, 26, 4, 27, 29, 31 | matecld 20232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥𝑀𝑦) ∈ (Base‘𝑃)) |
33 | | 0nn0 11307 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℕ0 |
34 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(coe1‘(𝑥𝑀𝑦)) = (coe1‘(𝑥𝑀𝑦)) |
35 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅) =
(Base‘𝑅) |
36 | 34, 26, 2, 35 | coe1fvalcl 19582 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥𝑀𝑦) ∈ (Base‘𝑃) ∧ 0 ∈ ℕ0) →
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
37 | 32, 33, 36 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
38 | 25, 37 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))) |
40 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
41 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) = (0g‘𝑅) |
42 | 2, 40, 35, 41 | coe1scl 19657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
(coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))) |
43 | 39, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
(coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))) |
44 | 43 | fveq1d 6193 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))‘𝑛)) |
45 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))) |
46 | | eqeq1 2626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0)) |
47 | 46 | ifbid 4108 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑛 → if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) |
49 | | nnnn0 11299 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
51 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
((coe1‘(𝑥𝑀𝑦))‘0) ∈ V |
52 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) ∈ V |
53 | 51, 52 | ifex 4156 |
. . . . . . . . . . . . . . 15
⊢ if(𝑛 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) ∈ V |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) ∈ V) |
55 | 45, 48, 50, 54 | fvmptd 6288 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))‘𝑛) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) |
56 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
57 | 56 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ¬
𝑛 = 0) |
58 | 57 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0) |
59 | 58 | iffalsed 4097 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) = (0g‘𝑅)) |
60 | 44, 55, 59 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = (0g‘𝑅)) |
61 | | eqcom 2629 |
. . . . . . . . . . . . 13
⊢
(((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) ↔ (0g‘𝑅) =
((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
62 | 61 | biimpi 206 |
. . . . . . . . . . . 12
⊢
(((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) → (0g‘𝑅) =
((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
63 | 60, 62 | sylan9eq 2676 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) ∧
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
64 | 63 | ex 450 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
(((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))) |
65 | 64 | ralimdva 2962 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) → ∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))) |
66 | 65 | imp 445 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) → ∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
67 | 38 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) → (𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))) |
68 | 2, 40, 35 | ply1sclid 19658 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
((coe1‘(𝑥𝑀𝑦))‘0) =
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0)) |
69 | 68 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)) |
70 | 67, 69 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)) |
71 | 66, 70 | jca 554 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0))) |
72 | 71 | ex 450 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
73 | 24, 72 | syl5bi 232 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
74 | 21, 73 | syld 47 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
75 | 9, 74 | mpd 15 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0))) |
76 | | c0ex 10034 |
. . . 4
⊢ 0 ∈
V |
77 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 0 →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) =
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0)) |
78 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 0 →
((coe1‘(𝑥𝑀𝑦))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘0)) |
79 | 77, 78 | eqeq12d 2637 |
. . . . 5
⊢ (𝑛 = 0 →
(((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0))) |
80 | 79 | ralunsn 4422 |
. . . 4
⊢ (0 ∈
V → (∀𝑛 ∈
(ℕ ∪ {0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
81 | 76, 80 | mp1i 13 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ (ℕ ∪
{0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
82 | 75, 81 | mpbird 247 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ (ℕ ∪
{0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
83 | | df-n0 11293 |
. . 3
⊢
ℕ0 = (ℕ ∪ {0}) |
84 | 83 | raleqi 3142 |
. 2
⊢
(∀𝑛 ∈
ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ ∀𝑛 ∈ (ℕ ∪
{0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
85 | 82, 84 | sylibr 224 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |