Step | Hyp | Ref
| Expression |
1 | | m2cpm.t |
. . . . . . . . 9
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
2 | | m2cpm.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | m2cpm.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2739 |
. . . . . . . . 9
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
5 | | eqid 2739 |
. . . . . . . . 9
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
6 | 1, 2, 3, 4, 5 | mat2pmatvalel 21489 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑀)𝑗) =
((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗))) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑖(𝑇‘𝑀)𝑗) =
((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗))) |
8 | 7 | fveq2d 6691 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
(coe1‘(𝑖(𝑇‘𝑀)𝑗)) =
(coe1‘((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗)))) |
9 | 8 | fveq1d 6689 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘(𝑖(𝑇‘𝑀)𝑗))‘𝑛) =
((coe1‘((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗)))‘𝑛)) |
10 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Ring) |
11 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
13 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁) |
14 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑀 ∈ 𝐵) |
15 | 2, 11, 3, 12, 13, 14 | matecld 21190 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖𝑀𝑗) ∈ (Base‘𝑅)) |
16 | 10, 15 | jca 515 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 ∈ Ring ∧ (𝑖𝑀𝑗) ∈ (Base‘𝑅))) |
17 | 16 | adantr 484 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑅 ∈ Ring ∧ (𝑖𝑀𝑗) ∈ (Base‘𝑅))) |
18 | | eqid 2739 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
19 | 4, 5, 11, 18 | coe1scl 21075 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑀𝑗) ∈ (Base‘𝑅)) →
(coe1‘((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, (𝑖𝑀𝑗), (0g‘𝑅)))) |
20 | 17, 19 | syl 17 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
(coe1‘((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, (𝑖𝑀𝑗), (0g‘𝑅)))) |
21 | | eqeq1 2743 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0)) |
22 | 21 | ifbid 4447 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → if(𝑘 = 0, (𝑖𝑀𝑗), (0g‘𝑅)) = if(𝑛 = 0, (𝑖𝑀𝑗), (0g‘𝑅))) |
23 | 22 | adantl 485 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring ∧
𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → if(𝑘 = 0, (𝑖𝑀𝑗), (0g‘𝑅)) = if(𝑛 = 0, (𝑖𝑀𝑗), (0g‘𝑅))) |
24 | | nnnn0 11996 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
25 | 24 | adantl 485 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
26 | | ovex 7216 |
. . . . . . . 8
⊢ (𝑖𝑀𝑗) ∈ V |
27 | | fvex 6700 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
28 | 26, 27 | ifex 4474 |
. . . . . . 7
⊢ if(𝑛 = 0, (𝑖𝑀𝑗), (0g‘𝑅)) ∈ V |
29 | 28 | a1i 11 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, (𝑖𝑀𝑗), (0g‘𝑅)) ∈ V) |
30 | 20, 23, 25, 29 | fvmptd 6795 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘((algSc‘(Poly1‘𝑅))‘(𝑖𝑀𝑗)))‘𝑛) = if(𝑛 = 0, (𝑖𝑀𝑗), (0g‘𝑅))) |
31 | | nnne0 11763 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
32 | 31 | neneqd 2940 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ¬
𝑛 = 0) |
33 | 32 | adantl 485 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0) |
34 | 33 | iffalsed 4435 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, (𝑖𝑀𝑗), (0g‘𝑅)) = (0g‘𝑅)) |
35 | 9, 30, 34 | 3eqtrd 2778 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑛 ∈ ℕ) →
((coe1‘(𝑖(𝑇‘𝑀)𝑗))‘𝑛) = (0g‘𝑅)) |
36 | 35 | ralrimiva 3097 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ∀𝑛 ∈ ℕ
((coe1‘(𝑖(𝑇‘𝑀)𝑗))‘𝑛) = (0g‘𝑅)) |
37 | 36 | ralrimivva 3104 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑛 ∈ ℕ
((coe1‘(𝑖(𝑇‘𝑀)𝑗))‘𝑛) = (0g‘𝑅)) |
38 | | eqid 2739 |
. . . 4
⊢ (𝑁 Mat
(Poly1‘𝑅))
= (𝑁 Mat
(Poly1‘𝑅)) |
39 | 1, 2, 3, 4, 38 | mat2pmatbas 21490 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
40 | | m2cpm.s |
. . . 4
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
41 | | eqid 2739 |
. . . 4
⊢
(Base‘(𝑁 Mat
(Poly1‘𝑅))) = (Base‘(𝑁 Mat (Poly1‘𝑅))) |
42 | 40, 4, 38, 41 | cpmatel 21475 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) → ((𝑇‘𝑀) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑛 ∈ ℕ
((coe1‘(𝑖(𝑇‘𝑀)𝑗))‘𝑛) = (0g‘𝑅))) |
43 | 39, 42 | syld3an3 1410 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑇‘𝑀) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑛 ∈ ℕ
((coe1‘(𝑖(𝑇‘𝑀)𝑗))‘𝑛) = (0g‘𝑅))) |
44 | 37, 43 | mpbird 260 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝑆) |