Step | Hyp | Ref
| Expression |
1 | | mat2pmatbas.t |
. . 3
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
2 | | mat2pmatbas.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | mat2pmatbas.b |
. . 3
⊢ 𝐵 = (Base‘𝐴) |
4 | | mat2pmatbas.p |
. . 3
⊢ 𝑃 = (Poly1‘𝑅) |
5 | | mat2pmatbas.c |
. . 3
⊢ 𝐶 = (𝑁 Mat 𝑃) |
6 | | mat2pmatbas0.h |
. . 3
⊢ 𝐻 = (Base‘𝐶) |
7 | 1, 2, 3, 4, 5, 6 | mat2pmatf 21877 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵⟶𝐻) |
8 | | simpl 483 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
9 | 8 | anim2i 617 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
10 | | df-3an 1088 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝐵)) |
11 | 9, 10 | sylibr 233 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵)) |
12 | | eqid 2738 |
. . . . . . . . 9
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
13 | 1, 2, 3, 4, 12 | mat2pmatvalel 21874 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑥)𝑗) = ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
14 | 11, 13 | sylan 580 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑥)𝑗) = ((algSc‘𝑃)‘(𝑖𝑥𝑗))) |
15 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
16 | 15 | anim2i 617 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
17 | | df-3an 1088 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝐵)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵)) |
19 | 1, 2, 3, 4, 12 | mat2pmatvalel 21874 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑦)𝑗) = ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
20 | 18, 19 | sylan 580 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇‘𝑦)𝑗) = ((algSc‘𝑃)‘(𝑖𝑦𝑗))) |
21 | 14, 20 | eqeq12d 2754 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑖(𝑇‘𝑥)𝑗) = (𝑖(𝑇‘𝑦)𝑗) ↔ ((algSc‘𝑃)‘(𝑖𝑥𝑗)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) |
22 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
23 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑃) |
24 | 4, 12, 22, 23 | ply1sclf1 21460 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(algSc‘𝑃):(Base‘𝑅)–1-1→(Base‘𝑃)) |
25 | 24 | ad3antlr 728 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (algSc‘𝑃):(Base‘𝑅)–1-1→(Base‘𝑃)) |
26 | | simprl 768 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
27 | | simprr 770 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁) |
28 | | simplrl 774 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑥 ∈ 𝐵) |
29 | 2, 22, 3, 26, 27, 28 | matecld 21575 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖𝑥𝑗) ∈ (Base‘𝑅)) |
30 | | simplrr 775 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑦 ∈ 𝐵) |
31 | 2, 22, 3, 26, 27, 30 | matecld 21575 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖𝑦𝑗) ∈ (Base‘𝑅)) |
32 | | f1veqaeq 7130 |
. . . . . . 7
⊢
(((algSc‘𝑃):(Base‘𝑅)–1-1→(Base‘𝑃) ∧ ((𝑖𝑥𝑗) ∈ (Base‘𝑅) ∧ (𝑖𝑦𝑗) ∈ (Base‘𝑅))) → (((algSc‘𝑃)‘(𝑖𝑥𝑗)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)) → (𝑖𝑥𝑗) = (𝑖𝑦𝑗))) |
33 | 25, 29, 31, 32 | syl12anc 834 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (((algSc‘𝑃)‘(𝑖𝑥𝑗)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)) → (𝑖𝑥𝑗) = (𝑖𝑦𝑗))) |
34 | 21, 33 | sylbid 239 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑖(𝑇‘𝑥)𝑗) = (𝑖(𝑇‘𝑦)𝑗) → (𝑖𝑥𝑗) = (𝑖𝑦𝑗))) |
35 | 34 | ralimdvva 3126 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖(𝑇‘𝑥)𝑗) = (𝑖(𝑇‘𝑦)𝑗) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑥𝑗) = (𝑖𝑦𝑗))) |
36 | 1, 2, 3, 4, 5, 6 | mat2pmatbas0 21876 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ 𝐻) |
37 | 11, 36 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) ∈ 𝐻) |
38 | 1, 2, 3, 4, 5, 6 | mat2pmatbas0 21876 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) ∈ 𝐻) |
39 | 18, 38 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) ∈ 𝐻) |
40 | 5, 6 | eqmat 21573 |
. . . . 5
⊢ (((𝑇‘𝑥) ∈ 𝐻 ∧ (𝑇‘𝑦) ∈ 𝐻) → ((𝑇‘𝑥) = (𝑇‘𝑦) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖(𝑇‘𝑥)𝑗) = (𝑖(𝑇‘𝑦)𝑗))) |
41 | 37, 39, 40 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥) = (𝑇‘𝑦) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖(𝑇‘𝑥)𝑗) = (𝑖(𝑇‘𝑦)𝑗))) |
42 | 2, 3 | eqmat 21573 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑥𝑗) = (𝑖𝑦𝑗))) |
43 | 42 | adantl 482 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑥𝑗) = (𝑖𝑦𝑗))) |
44 | 35, 41, 43 | 3imtr4d 294 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥) = (𝑇‘𝑦) → 𝑥 = 𝑦)) |
45 | 44 | ralrimivva 3123 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑇‘𝑥) = (𝑇‘𝑦) → 𝑥 = 𝑦)) |
46 | | dff13 7128 |
. 2
⊢ (𝑇:𝐵–1-1→𝐻 ↔ (𝑇:𝐵⟶𝐻 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑇‘𝑥) = (𝑇‘𝑦) → 𝑥 = 𝑦))) |
47 | 7, 45, 46 | sylanbrc 583 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–1-1→𝐻) |