Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’ (π ConstPolyMat π
) = (π ConstPolyMat π
) |
2 | | m2cpminvid.t |
. . . 4
β’ π = (π matToPolyMat π
) |
3 | | m2cpminvid.a |
. . . 4
β’ π΄ = (π Mat π
) |
4 | | m2cpminvid.k |
. . . 4
β’ πΎ = (Baseβπ΄) |
5 | 1, 2, 3, 4 | m2cpm 22243 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β (πβπ) β (π ConstPolyMat π
)) |
6 | | m2cpminvid.i |
. . . 4
β’ πΌ = (π cPolyMatToMat π
) |
7 | 6, 1 | cpm2mval 22252 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ (πβπ) β (π ConstPolyMat π
)) β (πΌβ(πβπ)) = (π₯ β π, π¦ β π β¦ ((coe1β(π₯(πβπ)π¦))β0))) |
8 | 5, 7 | syld3an3 1410 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β (πΌβ(πβπ)) = (π₯ β π, π¦ β π β¦ ((coe1β(π₯(πβπ)π¦))β0))) |
9 | | eqid 2733 |
. . . . . . . 8
β’
(Poly1βπ
) = (Poly1βπ
) |
10 | | eqid 2733 |
. . . . . . . 8
β’
(algScβ(Poly1βπ
)) =
(algScβ(Poly1βπ
)) |
11 | 2, 3, 4, 9, 10 | mat2pmatvalel 22227 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π₯ β π β§ π¦ β π)) β (π₯(πβπ)π¦) =
((algScβ(Poly1βπ
))β(π₯ππ¦))) |
12 | 11 | 3impb 1116 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β (π₯(πβπ)π¦) =
((algScβ(Poly1βπ
))β(π₯ππ¦))) |
13 | 12 | fveq2d 6896 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β (coe1β(π₯(πβπ)π¦)) =
(coe1β((algScβ(Poly1βπ
))β(π₯ππ¦)))) |
14 | 13 | fveq1d 6894 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β ((coe1β(π₯(πβπ)π¦))β0) =
((coe1β((algScβ(Poly1βπ
))β(π₯ππ¦)))β0)) |
15 | | simp12 1205 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β π
β Ring) |
16 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
17 | | simp2 1138 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β π₯ β π) |
18 | | simp3 1139 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β π¦ β π) |
19 | | simp13 1206 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β π β πΎ) |
20 | 3, 16, 4, 17, 18, 19 | matecld 21928 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) β (Baseβπ
)) |
21 | 9, 10, 16 | ply1sclid 21810 |
. . . . 5
β’ ((π
β Ring β§ (π₯ππ¦) β (Baseβπ
)) β (π₯ππ¦) =
((coe1β((algScβ(Poly1βπ
))β(π₯ππ¦)))β0)) |
22 | 15, 20, 21 | syl2anc 585 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) =
((coe1β((algScβ(Poly1βπ
))β(π₯ππ¦)))β0)) |
23 | 14, 22 | eqtr4d 2776 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ π₯ β π β§ π¦ β π) β ((coe1β(π₯(πβπ)π¦))β0) = (π₯ππ¦)) |
24 | 23 | mpoeq3dva 7486 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β (π₯ β π, π¦ β π β¦ ((coe1β(π₯(πβπ)π¦))β0)) = (π₯ β π, π¦ β π β¦ (π₯ππ¦))) |
25 | | eqidd 2734 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π β π β§ π β π)) β (π₯ β π, π¦ β π β¦ (π₯ππ¦)) = (π₯ β π, π¦ β π β¦ (π₯ππ¦))) |
26 | | oveq12 7418 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = π) β (π₯ππ¦) = (πππ)) |
27 | 26 | adantl 483 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π β π β§ π β π)) β§ (π₯ = π β§ π¦ = π)) β (π₯ππ¦) = (πππ)) |
28 | | simprl 770 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π β π β§ π β π)) β π β π) |
29 | | simprr 772 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π β π β§ π β π)) β π β π) |
30 | | ovexd 7444 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π β π β§ π β π)) β (πππ) β V) |
31 | 25, 27, 28, 29, 30 | ovmpod 7560 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β πΎ) β§ (π β π β§ π β π)) β (π(π₯ β π, π¦ β π β¦ (π₯ππ¦))π) = (πππ)) |
32 | 31 | ralrimivva 3201 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β βπ β π βπ β π (π(π₯ β π, π¦ β π β¦ (π₯ππ¦))π) = (πππ)) |
33 | | simp1 1137 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β π β Fin) |
34 | | simp2 1138 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β π
β Ring) |
35 | 3, 16, 4, 33, 34, 20 | matbas2d 21925 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β (π₯ β π, π¦ β π β¦ (π₯ππ¦)) β πΎ) |
36 | | simp3 1139 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β π β πΎ) |
37 | 3, 4 | eqmat 21926 |
. . . 4
β’ (((π₯ β π, π¦ β π β¦ (π₯ππ¦)) β πΎ β§ π β πΎ) β ((π₯ β π, π¦ β π β¦ (π₯ππ¦)) = π β βπ β π βπ β π (π(π₯ β π, π¦ β π β¦ (π₯ππ¦))π) = (πππ))) |
38 | 35, 36, 37 | syl2anc 585 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β ((π₯ β π, π¦ β π β¦ (π₯ππ¦)) = π β βπ β π βπ β π (π(π₯ β π, π¦ β π β¦ (π₯ππ¦))π) = (πππ))) |
39 | 32, 38 | mpbird 257 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β (π₯ β π, π¦ β π β¦ (π₯ππ¦)) = π) |
40 | 8, 24, 39 | 3eqtrd 2777 |
1
β’ ((π β Fin β§ π
β Ring β§ π β πΎ) β (πΌβ(πβπ)) = π) |