Step | Hyp | Ref
| Expression |
1 | | pm2mpval.p |
. . 3
β’ π = (Poly1βπ
) |
2 | | pm2mpval.c |
. . 3
β’ πΆ = (π Mat π) |
3 | | pm2mpval.b |
. . 3
β’ π΅ = (BaseβπΆ) |
4 | | pm2mpval.m |
. . 3
β’ β = (
Β·π βπ) |
5 | | pm2mpval.e |
. . 3
β’ β =
(.gβ(mulGrpβπ)) |
6 | | pm2mpval.x |
. . 3
β’ π = (var1βπ΄) |
7 | | pm2mpval.a |
. . 3
β’ π΄ = (π Mat π
) |
8 | | pm2mpval.q |
. . 3
β’ π = (Poly1βπ΄) |
9 | | pm2mpval.t |
. . 3
β’ π = (π pMatToMatPoly π
) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pm2mpfval 22161 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) = (π Ξ£g (π β β0
β¦ ((π decompPMat
π) β (π β π))))) |
11 | | pm2mpcl.l |
. . 3
β’ πΏ = (Baseβπ) |
12 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
13 | 7 | matring 21808 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
14 | 8 | ply1ring 21635 |
. . . . 5
β’ (π΄ β Ring β π β Ring) |
15 | | ringcmn 20008 |
. . . . 5
β’ (π β Ring β π β CMnd) |
16 | 13, 14, 15 | 3syl 18 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β π β CMnd) |
17 | 16 | 3adant3 1133 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β CMnd) |
18 | | nn0ex 12424 |
. . . 4
β’
β0 β V |
19 | 18 | a1i 11 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β β0 β
V) |
20 | 13 | 3adant3 1133 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π΄ β Ring) |
21 | 20 | adantr 482 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β π΄ β Ring) |
22 | | simpl2 1193 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β π
β Ring) |
23 | | simpl3 1194 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β π β π΅) |
24 | | simpr 486 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β π β
β0) |
25 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ΄) =
(Baseβπ΄) |
26 | 1, 2, 3, 7, 25 | decpmatcl 22132 |
. . . . . 6
β’ ((π
β Ring β§ π β π΅ β§ π β β0) β (π decompPMat π) β (Baseβπ΄)) |
27 | 22, 23, 24, 26 | syl3anc 1372 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β (π decompPMat π) β (Baseβπ΄)) |
28 | | eqid 2733 |
. . . . . 6
β’
(mulGrpβπ) =
(mulGrpβπ) |
29 | 25, 8, 6, 4, 28, 5,
11 | ply1tmcl 21659 |
. . . . 5
β’ ((π΄ β Ring β§ (π decompPMat π) β (Baseβπ΄) β§ π β β0) β ((π decompPMat π) β (π β π)) β πΏ) |
30 | 21, 27, 24, 29 | syl3anc 1372 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β ((π decompPMat π) β (π β π)) β πΏ) |
31 | 30 | fmpttd 7064 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β β0 β¦ ((π decompPMat π) β (π β π))):β0βΆπΏ) |
32 | 8 | ply1lmod 21639 |
. . . . 5
β’ (π΄ β Ring β π β LMod) |
33 | 20, 32 | syl 17 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β LMod) |
34 | | eqidd 2734 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (Scalarβπ) = (Scalarβπ)) |
35 | 8, 6, 28, 5, 11 | ply1moncl 21658 |
. . . . 5
β’ ((π΄ β Ring β§ π β β0)
β (π β π) β πΏ) |
36 | 20, 35 | sylan 581 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β β0) β (π β π) β πΏ) |
37 | | eqid 2733 |
. . . 4
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
38 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ΄) = (0gβπ΄) |
39 | 1, 2, 3, 7, 38 | decpmatfsupp 22134 |
. . . . . 6
β’ ((π
β Ring β§ π β π΅) β (π β β0 β¦ (π decompPMat π)) finSupp (0gβπ΄)) |
40 | 39 | 3adant1 1131 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β β0 β¦ (π decompPMat π)) finSupp (0gβπ΄)) |
41 | 8 | ply1sca 21640 |
. . . . . . . 8
β’ (π΄ β Ring β π΄ = (Scalarβπ)) |
42 | 41 | eqcomd 2739 |
. . . . . . 7
β’ (π΄ β Ring β
(Scalarβπ) = π΄) |
43 | 20, 42 | syl 17 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (Scalarβπ) = π΄) |
44 | 43 | fveq2d 6847 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β
(0gβ(Scalarβπ)) = (0gβπ΄)) |
45 | 40, 44 | breqtrrd 5134 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β β0 β¦ (π decompPMat π)) finSupp
(0gβ(Scalarβπ))) |
46 | 19, 33, 34, 11, 27, 36, 12, 37, 4, 45 | mptscmfsupp0 20402 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β β0 β¦ ((π decompPMat π) β (π β π))) finSupp (0gβπ)) |
47 | 11, 12, 17, 19, 31, 46 | gsumcl 19697 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π Ξ£g (π β β0
β¦ ((π decompPMat
π) β (π β π)))) β πΏ) |
48 | 10, 47 | eqeltrd 2834 |
1
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β πΏ) |