Step | Hyp | Ref
| Expression |
1 | | m2cpmfo.s |
. . 3
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
2 | | m2cpmfo.t |
. . 3
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
3 | | m2cpmfo.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
4 | | m2cpmfo.k |
. . 3
⊢ 𝐾 = (Base‘𝐴) |
5 | 1, 2, 3, 4 | m2cpmf 21486 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐾⟶𝑆) |
6 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
7 | | simplll 775 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) → 𝑁 ∈ Fin) |
8 | | simpllr 776 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) → 𝑅 ∈ Ring) |
9 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑁 Mat
(Poly1‘𝑅))
= (𝑁 Mat
(Poly1‘𝑅)) |
10 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
11 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘(𝑁 Mat
(Poly1‘𝑅))) = (Base‘(𝑁 Mat (Poly1‘𝑅))) |
12 | | simp2 1138 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
13 | | simp3 1139 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
14 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
15 | 1, 14, 9, 11 | cpmatpmat 21454 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝑆) → 𝑚 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
16 | 15 | ad4ant124 1174 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) → 𝑚 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑚 ∈ (Base‘(𝑁 Mat (Poly1‘𝑅)))) |
18 | 9, 10, 11, 12, 13, 17 | matecld 21170 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑚𝑗) ∈
(Base‘(Poly1‘𝑅))) |
19 | | 0nn0 11984 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
20 | | eqid 2738 |
. . . . . . . . 9
⊢
(coe1‘(𝑖𝑚𝑗)) = (coe1‘(𝑖𝑚𝑗)) |
21 | 20, 10, 14, 6 | coe1fvalcl 20980 |
. . . . . . . 8
⊢ (((𝑖𝑚𝑗) ∈
(Base‘(Poly1‘𝑅)) ∧ 0 ∈ ℕ0)
→ ((coe1‘(𝑖𝑚𝑗))‘0) ∈ (Base‘𝑅)) |
22 | 18, 19, 21 | sylancl 589 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝑚𝑗))‘0) ∈ (Base‘𝑅)) |
23 | 3, 6, 4, 7, 8, 22 | matbas2d 21167 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ 𝑆) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)) ∈ 𝐾) |
24 | 23 | fmpttd 6883 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → (𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0))):𝑆⟶𝐾) |
25 | | simpr 488 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
26 | 24, 25 | ffvelrnd 6856 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥) ∈ 𝐾) |
27 | | fveq2 6668 |
. . . . . 6
⊢ (𝑐 = ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥) → (𝑇‘𝑐) = (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥))) |
28 | 27 | eqeq2d 2749 |
. . . . 5
⊢ (𝑐 = ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥) → (𝑥 = (𝑇‘𝑐) ↔ 𝑥 = (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)))) |
29 | 28 | adantl 485 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) ∧ 𝑐 = ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)) → (𝑥 = (𝑇‘𝑐) ↔ 𝑥 = (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)))) |
30 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑁 cPolyMatToMat 𝑅) = (𝑁 cPolyMatToMat 𝑅) |
31 | 30, 1 | cpm2mfval 21493 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))) |
32 | 31 | fveq1d 6670 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑁 cPolyMatToMat 𝑅)‘𝑥) = ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)) |
33 | 32 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → ((𝑁 cPolyMatToMat 𝑅)‘𝑥) = ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)) |
34 | 33 | eqcomd 2744 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → ((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥) = ((𝑁 cPolyMatToMat 𝑅)‘𝑥)) |
35 | 34 | fveq2d 6672 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)) = (𝑇‘((𝑁 cPolyMatToMat 𝑅)‘𝑥))) |
36 | 1, 30, 2 | m2cpminvid2 21499 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → (𝑇‘((𝑁 cPolyMatToMat 𝑅)‘𝑥)) = 𝑥) |
37 | 35, 36 | eqtrd 2773 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)) = 𝑥) |
38 | 37 | 3expa 1119 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥)) = 𝑥) |
39 | 38 | eqcomd 2744 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑇‘((𝑚 ∈ 𝑆 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝑚𝑗))‘0)))‘𝑥))) |
40 | 26, 29, 39 | rspcedvd 3527 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 𝑥 = (𝑇‘𝑐)) |
41 | 40 | ralrimiva 3096 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝑆 ∃𝑐 ∈ 𝐾 𝑥 = (𝑇‘𝑐)) |
42 | | dffo3 6872 |
. 2
⊢ (𝑇:𝐾–onto→𝑆 ↔ (𝑇:𝐾⟶𝑆 ∧ ∀𝑥 ∈ 𝑆 ∃𝑐 ∈ 𝐾 𝑥 = (𝑇‘𝑐))) |
43 | 5, 41, 42 | sylanbrc 586 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐾–onto→𝑆) |