| Step | Hyp | Ref
| Expression |
| 1 | | m2cpminvid2lem.s |
. . . . . . . 8
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
| 2 | | m2cpminvid2lem.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃) |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝑁 Mat
𝑃)) = (Base‘(𝑁 Mat 𝑃)) |
| 5 | 1, 2, 3, 4 | cpmatelimp 22718 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)))) |
| 6 | 5 | 3impia 1118 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑀 ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))) |
| 7 | 6 | simprd 495 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)) |
| 8 | 7 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)) |
| 9 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑥𝑀𝑗))) |
| 10 | 9 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑘) = ((coe1‘(𝑥𝑀𝑗))‘𝑘)) |
| 11 | 10 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑖 = 𝑥 → (((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅))) |
| 12 | 11 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑖 = 𝑥 → (∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅))) |
| 13 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑦 → (𝑥𝑀𝑗) = (𝑥𝑀𝑦)) |
| 14 | 13 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → (coe1‘(𝑥𝑀𝑗)) = (coe1‘(𝑥𝑀𝑦))) |
| 15 | 14 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((coe1‘(𝑥𝑀𝑗))‘𝑘) = ((coe1‘(𝑥𝑀𝑦))‘𝑘)) |
| 16 | 15 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑗 = 𝑦 → (((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
| 17 | 16 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑗 = 𝑦 → (∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑗))‘𝑘) = (0g‘𝑅) ↔ ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
| 18 | 12, 17 | rspc2v 3633 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) → ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
| 19 | 18 | adantl 481 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) → ∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅))) |
| 20 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅) ↔ ((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅))) |
| 21 | 20 | cbvralvw 3237 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅) ↔ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) |
| 22 | | simpl2 1193 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑅 ∈ Ring) |
| 23 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 24 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑥 ∈ 𝑁) |
| 25 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑦 ∈ 𝑁) |
| 26 | 1, 2, 3, 4 | cpmatpmat 22716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ (Base‘(𝑁 Mat 𝑃))) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑀 ∈ (Base‘(𝑁 Mat 𝑃))) |
| 28 | 3, 23, 4, 24, 25, 27 | matecld 22432 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥𝑀𝑦) ∈ (Base‘𝑃)) |
| 29 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℕ0 |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(coe1‘(𝑥𝑀𝑦)) = (coe1‘(𝑥𝑀𝑦)) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 32 | 30, 23, 2, 31 | coe1fvalcl 22214 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥𝑀𝑦) ∈ (Base‘𝑃) ∧ 0 ∈ ℕ0) →
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
| 33 | 28, 29, 32 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
| 34 | 22, 33 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 38 | 2, 36, 31, 37 | coe1scl 22290 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
(coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))) |
| 39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
(coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))) |
| 40 | 39 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))‘𝑛)) |
| 41 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))) |
| 42 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0)) |
| 43 | 42 | ifbid 4549 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑛 → if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 = 𝑛) → if(𝑙 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) |
| 45 | | nnnn0 12533 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
| 47 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢
((coe1‘(𝑥𝑀𝑦))‘0) ∈ V |
| 48 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) ∈ V |
| 49 | 47, 48 | ifex 4576 |
. . . . . . . . . . . . . . 15
⊢ if(𝑛 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) ∈ V |
| 50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) ∈ V) |
| 51 | 41, 44, 46, 50 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ0 ↦ if(𝑙 = 0,
((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)))‘𝑛) = if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅))) |
| 52 | | nnne0 12300 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
| 53 | 52 | neneqd 2945 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ¬
𝑛 = 0) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0) |
| 55 | 54 | iffalsed 4536 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, ((coe1‘(𝑥𝑀𝑦))‘0), (0g‘𝑅)) = (0g‘𝑅)) |
| 56 | 40, 51, 55 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = (0g‘𝑅)) |
| 57 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢
(((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) ↔ (0g‘𝑅) =
((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
| 58 | 57 | biimpi 216 |
. . . . . . . . . . . 12
⊢
(((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) → (0g‘𝑅) =
((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
| 59 | 56, 58 | sylan9eq 2797 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) ∧
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
| 60 | 59 | ex 412 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
(((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))) |
| 61 | 60 | ralimdva 3167 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) → ∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))) |
| 62 | 61 | imp 406 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) → ∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
| 63 | 34 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) → (𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅))) |
| 64 | 2, 36, 31 | ply1sclid 22291 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
((coe1‘(𝑥𝑀𝑦))‘0) =
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0)) |
| 65 | 64 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)) |
| 66 | 63, 65 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)) |
| 67 | 62, 66 | jca 511 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ ∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅)) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0))) |
| 68 | 67 | ex 412 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑛) = (0g‘𝑅) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
| 69 | 21, 68 | biimtrid 242 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑘 ∈ ℕ
((coe1‘(𝑥𝑀𝑦))‘𝑘) = (0g‘𝑅) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
| 70 | 19, 69 | syld 47 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
| 71 | 8, 70 | mpd 15 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0))) |
| 72 | | c0ex 11255 |
. . . 4
⊢ 0 ∈
V |
| 73 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = 0 →
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) =
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0)) |
| 74 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = 0 →
((coe1‘(𝑥𝑀𝑦))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘0)) |
| 75 | 73, 74 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 0 →
(((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0))) |
| 76 | 75 | ralunsn 4894 |
. . . 4
⊢ (0 ∈
V → (∀𝑛 ∈
(ℕ ∪ {0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
| 77 | 72, 76 | mp1i 13 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (∀𝑛 ∈ (ℕ ∪
{0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ (∀𝑛 ∈ ℕ
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ∧
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘0) =
((coe1‘(𝑥𝑀𝑦))‘0)))) |
| 78 | 71, 77 | mpbird 257 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ (ℕ ∪
{0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
| 79 | | df-n0 12527 |
. . 3
⊢
ℕ0 = (ℕ ∪ {0}) |
| 80 | 79 | raleqi 3324 |
. 2
⊢
(∀𝑛 ∈
ℕ0 ((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔ ∀𝑛 ∈ (ℕ ∪
{0})((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
| 81 | 78, 80 | sylibr 234 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0
((coe1‘((algSc‘𝑃)‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |