Step | Hyp | Ref
| Expression |
1 | | m2cpminvid2.i |
. . . 4
⊢ 𝐼 = (𝑁 cPolyMatToMat 𝑅) |
2 | | m2cpminvid2.s |
. . . 4
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
3 | 1, 2 | cpm2mval 21647 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝐼‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))) |
4 | 3 | fveq2d 6721 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑇‘(𝐼‘𝑀)) = (𝑇‘(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0)))) |
5 | | simp1 1138 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → 𝑁 ∈ Fin) |
6 | | simp2 1139 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → 𝑅 ∈ Ring) |
7 | | eqid 2737 |
. . . . 5
⊢ (𝑁 Mat 𝑅) = (𝑁 Mat 𝑅) |
8 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
9 | | eqid 2737 |
. . . . 5
⊢
(Base‘(𝑁 Mat
𝑅)) = (Base‘(𝑁 Mat 𝑅)) |
10 | | eqid 2737 |
. . . . . . 7
⊢ (𝑁 Mat
(Poly1‘𝑅))
= (𝑁 Mat
(Poly1‘𝑅)) |
11 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
12 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑁 Mat
(Poly1‘𝑅))) = (Base‘(𝑁 Mat (Poly1‘𝑅))) |
13 | | simp2 1139 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
14 | | simp3 1140 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁) |
15 | | eqid 2737 |
. . . . . . . . 9
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
16 | 2, 15, 10, 12 | cpmatpmat 21607 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
17 | 16 | 3ad2ant1 1135 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑀 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
18 | 10, 11, 12, 13, 14, 17 | matecld 21323 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (𝑥𝑀𝑦) ∈
(Base‘(Poly1‘𝑅))) |
19 | | 0nn0 12105 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
20 | | eqid 2737 |
. . . . . . 7
⊢
(coe1‘(𝑥𝑀𝑦)) = (coe1‘(𝑥𝑀𝑦)) |
21 | 20, 11, 15, 8 | coe1fvalcl 21133 |
. . . . . 6
⊢ (((𝑥𝑀𝑦) ∈
(Base‘(Poly1‘𝑅)) ∧ 0 ∈ ℕ0)
→ ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
22 | 18, 19, 21 | sylancl 589 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
23 | 7, 8, 9, 5, 6, 22 | matbas2d 21320 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0)) ∈ (Base‘(𝑁 Mat 𝑅))) |
24 | | m2cpminvid2.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
25 | | eqid 2737 |
. . . . 5
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
26 | 24, 7, 9, 15, 25 | mat2pmatval 21621 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0)) ∈ (Base‘(𝑁 Mat 𝑅))) → (𝑇‘(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘(𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))𝑗)))) |
27 | 5, 6, 23, 26 | syl3anc 1373 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑇‘(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘(𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))𝑗)))) |
28 | | eqidd 2738 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))) |
29 | | oveq12 7222 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (𝑥𝑀𝑦) = (𝑖𝑀𝑗)) |
30 | 29 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (coe1‘(𝑥𝑀𝑦)) = (coe1‘(𝑖𝑀𝑗))) |
31 | 30 | fveq1d 6719 |
. . . . . . 7
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → ((coe1‘(𝑥𝑀𝑦))‘0) = ((coe1‘(𝑖𝑀𝑗))‘0)) |
32 | 31 | adantl 485 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ (𝑥 = 𝑖 ∧ 𝑦 = 𝑗)) → ((coe1‘(𝑥𝑀𝑦))‘0) = ((coe1‘(𝑖𝑀𝑗))‘0)) |
33 | | simp2 1139 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
34 | | simp3 1140 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
35 | | fvexd 6732 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝑀𝑗))‘0) ∈ V) |
36 | 28, 32, 33, 34, 35 | ovmpod 7361 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))𝑗) = ((coe1‘(𝑖𝑀𝑗))‘0)) |
37 | 36 | fveq2d 6721 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) →
((algSc‘(Poly1‘𝑅))‘(𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))𝑗)) =
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) |
38 | 37 | mpoeq3dva 7288 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘(𝑖(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))) |
39 | 27, 38 | eqtrd 2777 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑇‘(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe1‘(𝑥𝑀𝑦))‘0))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))) |
40 | 2, 15 | m2cpminvid2lem 21651 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ∀𝑛 ∈ ℕ0
((coe1‘((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛)) |
41 | | simpl2 1194 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑅 ∈ Ring) |
42 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑥 ∈ 𝑁) |
43 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑦 ∈ 𝑁) |
44 | 16 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑀 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
45 | 10, 11, 12, 42, 43, 44 | matecld 21323 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥𝑀𝑦) ∈
(Base‘(Poly1‘𝑅))) |
46 | 45, 19, 21 | sylancl 589 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) |
47 | 15, 25, 8, 11 | ply1sclcl 21207 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑥𝑀𝑦))‘0) ∈ (Base‘𝑅)) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) ∈
(Base‘(Poly1‘𝑅))) |
48 | 41, 46, 47 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) ∈
(Base‘(Poly1‘𝑅))) |
49 | | eqid 2737 |
. . . . . . . . 9
⊢
(coe1‘((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0))) =
(coe1‘((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0))) |
50 | 15, 11, 49, 20 | ply1coe1eq 21219 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) ∈
(Base‘(Poly1‘𝑅)) ∧ (𝑥𝑀𝑦) ∈
(Base‘(Poly1‘𝑅))) → (∀𝑛 ∈ ℕ0
((coe1‘((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛) ↔
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦))) |
51 | 50 | bicomd 226 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) ∈
(Base‘(Poly1‘𝑅)) ∧ (𝑥𝑀𝑦) ∈
(Base‘(Poly1‘𝑅))) →
(((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦) ↔ ∀𝑛 ∈ ℕ0
((coe1‘((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))) |
52 | 41, 48, 45, 51 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) →
(((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦) ↔ ∀𝑛 ∈ ℕ0
((coe1‘((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)))‘𝑛) = ((coe1‘(𝑥𝑀𝑦))‘𝑛))) |
53 | 40, 52 | mpbird 260 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦)) |
54 | 53 | ralrimivva 3112 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 ((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦)) |
55 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))) |
56 | | oveq12 7222 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑖𝑀𝑗) = (𝑥𝑀𝑦)) |
57 | 56 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑥𝑀𝑦))) |
58 | 57 | fveq1d 6719 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → ((coe1‘(𝑖𝑀𝑗))‘0) = ((coe1‘(𝑥𝑀𝑦))‘0)) |
59 | 58 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)) =
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0))) |
60 | 59 | adantl 485 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) ∧ (𝑖 = 𝑥 ∧ 𝑗 = 𝑦)) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)) =
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0))) |
61 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
62 | | simpr 488 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁) |
63 | | fvexd 6732 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) ∈ V) |
64 | 55, 60, 61, 62, 63 | ovmpod 7361 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) =
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0))) |
65 | 64 | eqeq1d 2739 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → ((𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) = (𝑥𝑀𝑦) ↔
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦))) |
66 | 65 | anasss 470 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → ((𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) = (𝑥𝑀𝑦) ↔
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦))) |
67 | 66 | 2ralbidva 3119 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) = (𝑥𝑀𝑦) ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 ((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑥𝑀𝑦))‘0)) = (𝑥𝑀𝑦))) |
68 | 54, 67 | mpbird 260 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) = (𝑥𝑀𝑦)) |
69 | | fvexd 6732 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (Poly1‘𝑅) ∈ V) |
70 | 6 | 3ad2ant1 1135 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
71 | 16 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
72 | 10, 11, 12, 33, 34, 71 | matecld 21323 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑀𝑗) ∈
(Base‘(Poly1‘𝑅))) |
73 | | eqid 2737 |
. . . . . . . 8
⊢
(coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑖𝑀𝑗)) |
74 | 73, 11, 15, 8 | coe1fvalcl 21133 |
. . . . . . 7
⊢ (((𝑖𝑀𝑗) ∈
(Base‘(Poly1‘𝑅)) ∧ 0 ∈ ℕ0)
→ ((coe1‘(𝑖𝑀𝑗))‘0) ∈ (Base‘𝑅)) |
75 | 72, 19, 74 | sylancl 589 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝑀𝑗))‘0) ∈ (Base‘𝑅)) |
76 | 15, 25, 8, 11 | ply1sclcl 21207 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((coe1‘(𝑖𝑀𝑗))‘0) ∈ (Base‘𝑅)) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)) ∈
(Base‘(Poly1‘𝑅))) |
77 | 70, 75, 76 | syl2anc 587 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) →
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)) ∈
(Base‘(Poly1‘𝑅))) |
78 | 10, 11, 12, 5, 69, 77 | matbas2d 21320 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) ∈ (Base‘(𝑁 Mat
(Poly1‘𝑅)))) |
79 | 10, 12 | eqmat 21321 |
. . . 4
⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) ∈ (Base‘(𝑁 Mat
(Poly1‘𝑅))) ∧ 𝑀 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) = 𝑀 ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) = (𝑥𝑀𝑦))) |
80 | 78, 16, 79 | syl2anc 587 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) = 𝑀 ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0)))𝑦) = (𝑥𝑀𝑦))) |
81 | 68, 80 | mpbird 260 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦
((algSc‘(Poly1‘𝑅))‘((coe1‘(𝑖𝑀𝑗))‘0))) = 𝑀) |
82 | 4, 39, 81 | 3eqtrd 2781 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) → (𝑇‘(𝐼‘𝑀)) = 𝑀) |