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 22100 |
. 2
β’ ((π β Fin β§ π
β Ring) β π:π΅βΆπ») |
8 | | simpl 484 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β§ π¦ β π΅) β π₯ β π΅) |
9 | 8 | anim2i 618 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β Fin β§ π
β Ring) β§ π₯ β π΅)) |
10 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π₯ β π΅) β ((π β Fin β§ π
β Ring) β§ π₯ β π΅)) |
11 | 9, 10 | sylibr 233 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ π₯ β π΅)) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(algScβπ) =
(algScβπ) |
13 | 1, 2, 3, 4, 12 | mat2pmatvalel 22097 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π₯ β π΅) β§ (π β π β§ π β π)) β (π(πβπ₯)π) = ((algScβπ)β(ππ₯π))) |
14 | 11, 13 | sylan 581 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (π(πβπ₯)π) = ((algScβπ)β(ππ₯π))) |
15 | | simpr 486 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β§ π¦ β π΅) β π¦ β π΅) |
16 | 15 | anim2i 618 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β Fin β§ π
β Ring) β§ π¦ β π΅)) |
17 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π¦ β π΅) β ((π β Fin β§ π
β Ring) β§ π¦ β π΅)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ π¦ β π΅)) |
19 | 1, 2, 3, 4, 12 | mat2pmatvalel 22097 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π¦ β π΅) β§ (π β π β§ π β π)) β (π(πβπ¦)π) = ((algScβπ)β(ππ¦π))) |
20 | 18, 19 | sylan 581 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (π(πβπ¦)π) = ((algScβπ)β(ππ¦π))) |
21 | 14, 20 | eqeq12d 2749 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β ((π(πβπ₯)π) = (π(πβπ¦)π) β ((algScβπ)β(ππ₯π)) = ((algScβπ)β(ππ¦π)))) |
22 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
23 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
24 | 4, 12, 22, 23 | ply1sclf1 21683 |
. . . . . . . 8
β’ (π
β Ring β
(algScβπ):(Baseβπ
)β1-1β(Baseβπ)) |
25 | 24 | ad3antlr 730 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (algScβπ):(Baseβπ
)β1-1β(Baseβπ)) |
26 | | simprl 770 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π β π) |
27 | | simprr 772 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π β π) |
28 | | simplrl 776 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π₯ β π΅) |
29 | 2, 22, 3, 26, 27, 28 | matecld 21798 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (ππ₯π) β (Baseβπ
)) |
30 | | simplrr 777 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π¦ β π΅) |
31 | 2, 22, 3, 26, 27, 30 | matecld 21798 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (ππ¦π) β (Baseβπ
)) |
32 | | f1veqaeq 7208 |
. . . . . . 7
β’
(((algScβπ):(Baseβπ
)β1-1β(Baseβπ) β§ ((ππ₯π) β (Baseβπ
) β§ (ππ¦π) β (Baseβπ
))) β (((algScβπ)β(ππ₯π)) = ((algScβπ)β(ππ¦π)) β (ππ₯π) = (ππ¦π))) |
33 | 25, 29, 31, 32 | syl12anc 836 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (((algScβπ)β(ππ₯π)) = ((algScβπ)β(ππ¦π)) β (ππ₯π) = (ππ¦π))) |
34 | 21, 33 | sylbid 239 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β ((π(πβπ₯)π) = (π(πβπ¦)π) β (ππ₯π) = (ππ¦π))) |
35 | 34 | ralimdvva 3198 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β π βπ β π (π(πβπ₯)π) = (π(πβπ¦)π) β βπ β π βπ β π (ππ₯π) = (ππ¦π))) |
36 | 1, 2, 3, 4, 5, 6 | mat2pmatbas0 22099 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π₯ β π΅) β (πβπ₯) β π») |
37 | 11, 36 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβπ₯) β π») |
38 | 1, 2, 3, 4, 5, 6 | mat2pmatbas0 22099 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π¦ β π΅) β (πβπ¦) β π») |
39 | 18, 38 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβπ¦) β π») |
40 | 5, 6 | eqmat 21796 |
. . . . 5
β’ (((πβπ₯) β π» β§ (πβπ¦) β π») β ((πβπ₯) = (πβπ¦) β βπ β π βπ β π (π(πβπ₯)π) = (π(πβπ¦)π))) |
41 | 37, 39, 40 | syl2anc 585 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβπ₯) = (πβπ¦) β βπ β π βπ β π (π(πβπ₯)π) = (π(πβπ¦)π))) |
42 | 2, 3 | eqmat 21796 |
. . . . 5
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ = π¦ β βπ β π βπ β π (ππ₯π) = (ππ¦π))) |
43 | 42 | adantl 483 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ = π¦ β βπ β π βπ β π (ππ₯π) = (ππ¦π))) |
44 | 35, 41, 43 | 3imtr4d 294 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
45 | 44 | ralrimivva 3194 |
. 2
β’ ((π β Fin β§ π
β Ring) β
βπ₯ β π΅ βπ¦ β π΅ ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
46 | | dff13 7206 |
. 2
β’ (π:π΅β1-1βπ» β (π:π΅βΆπ» β§ βπ₯ β π΅ βπ¦ β π΅ ((πβπ₯) = (πβπ¦) β π₯ = π¦))) |
47 | 7, 45, 46 | sylanbrc 584 |
1
β’ ((π β Fin β§ π
β Ring) β π:π΅β1-1βπ») |