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 22229 |
. 2
β’ ((π β Fin β§ π
β Ring) β π:π΅βΆπ») |
8 | | simpl 483 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β§ π¦ β π΅) β π₯ β π΅) |
9 | 8 | anim2i 617 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β Fin β§ π
β Ring) β§ π₯ β π΅)) |
10 | | df-3an 1089 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π₯ β π΅) β ((π β Fin β§ π
β Ring) β§ π₯ β π΅)) |
11 | 9, 10 | sylibr 233 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ π₯ β π΅)) |
12 | | eqid 2732 |
. . . . . . . . 9
β’
(algScβπ) =
(algScβπ) |
13 | 1, 2, 3, 4, 12 | mat2pmatvalel 22226 |
. . . . . . . 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 1089 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π¦ β π΅) β ((π β Fin β§ π
β Ring) β§ π¦ β π΅)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ π¦ β π΅)) |
19 | 1, 2, 3, 4, 12 | mat2pmatvalel 22226 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π¦ β π΅) β§ (π β π β§ π β π)) β (π(πβπ¦)π) = ((algScβπ)β(ππ¦π))) |
20 | 18, 19 | sylan 580 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (π(πβπ¦)π) = ((algScβπ)β(ππ¦π))) |
21 | 14, 20 | eqeq12d 2748 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β ((π(πβπ₯)π) = (π(πβπ¦)π) β ((algScβπ)β(ππ₯π)) = ((algScβπ)β(ππ¦π)))) |
22 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
23 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
24 | 4, 12, 22, 23 | ply1sclf1 21810 |
. . . . . . . 8
β’ (π
β Ring β
(algScβπ):(Baseβπ
)β1-1β(Baseβπ)) |
25 | 24 | ad3antlr 729 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (algScβπ):(Baseβπ
)β1-1β(Baseβπ)) |
26 | | simprl 769 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π β π) |
27 | | simprr 771 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π β π) |
28 | | simplrl 775 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π₯ β π΅) |
29 | 2, 22, 3, 26, 27, 28 | matecld 21927 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (ππ₯π) β (Baseβπ
)) |
30 | | simplrr 776 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β π¦ β π΅) |
31 | 2, 22, 3, 26, 27, 30 | matecld 21927 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (ππ¦π) β (Baseβπ
)) |
32 | | f1veqaeq 7255 |
. . . . . . 7
β’
(((algScβπ):(Baseβπ
)β1-1β(Baseβπ) β§ ((ππ₯π) β (Baseβπ
) β§ (ππ¦π) β (Baseβπ
))) β (((algScβπ)β(ππ₯π)) = ((algScβπ)β(ππ¦π)) β (ππ₯π) = (ππ¦π))) |
33 | 25, 29, 31, 32 | syl12anc 835 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β (((algScβπ)β(ππ₯π)) = ((algScβπ)β(ππ¦π)) β (ππ₯π) = (ππ¦π))) |
34 | 21, 33 | sylbid 239 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π β§ π β π)) β ((π(πβπ₯)π) = (π(πβπ¦)π) β (ππ₯π) = (ππ¦π))) |
35 | 34 | ralimdvva 3204 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β π βπ β π (π(πβπ₯)π) = (π(πβπ¦)π) β βπ β π βπ β π (ππ₯π) = (ππ¦π))) |
36 | 1, 2, 3, 4, 5, 6 | mat2pmatbas0 22228 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π₯ β π΅) β (πβπ₯) β π») |
37 | 11, 36 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβπ₯) β π») |
38 | 1, 2, 3, 4, 5, 6 | mat2pmatbas0 22228 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π¦ β π΅) β (πβπ¦) β π») |
39 | 18, 38 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβπ¦) β π») |
40 | 5, 6 | eqmat 21925 |
. . . . 5
β’ (((πβπ₯) β π» β§ (πβπ¦) β π») β ((πβπ₯) = (πβπ¦) β βπ β π βπ β π (π(πβπ₯)π) = (π(πβπ¦)π))) |
41 | 37, 39, 40 | syl2anc 584 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβπ₯) = (πβπ¦) β βπ β π βπ β π (π(πβπ₯)π) = (π(πβπ¦)π))) |
42 | 2, 3 | eqmat 21925 |
. . . . 5
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ = π¦ β βπ β π βπ β π (ππ₯π) = (ππ¦π))) |
43 | 42 | adantl 482 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ = π¦ β βπ β π βπ β π (ππ₯π) = (ππ¦π))) |
44 | 35, 41, 43 | 3imtr4d 293 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
45 | 44 | ralrimivva 3200 |
. 2
β’ ((π β Fin β§ π
β Ring) β
βπ₯ β π΅ βπ¦ β π΅ ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
46 | | dff13 7253 |
. 2
β’ (π:π΅β1-1βπ» β (π:π΅βΆπ» β§ βπ₯ β π΅ βπ¦ β π΅ ((πβπ₯) = (πβπ¦) β π₯ = π¦))) |
47 | 7, 45, 46 | sylanbrc 583 |
1
β’ ((π β Fin β§ π
β Ring) β π:π΅β1-1βπ») |