Step |
Hyp |
Ref |
Expression |
1 |
|
cpmidgsum.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
cpmidgsum.b |
โข ๐ต = ( Base โ ๐ด ) |
3 |
|
cpmidgsum.p |
โข ๐ = ( Poly1 โ ๐
) |
4 |
|
cpmidgsum.y |
โข ๐ = ( ๐ Mat ๐ ) |
5 |
|
cpmidgsum.x |
โข ๐ = ( var1 โ ๐
) |
6 |
|
cpmidgsum.e |
โข โ = ( .g โ ( mulGrp โ ๐ ) ) |
7 |
|
cpmidgsum.m |
โข ยท = ( ยท๐ โ ๐ ) |
8 |
|
cpmidgsum.1 |
โข 1 = ( 1r โ ๐ ) |
9 |
|
cpmidgsum.u |
โข ๐ = ( algSc โ ๐ ) |
10 |
|
cpmidgsum.c |
โข ๐ถ = ( ๐ CharPlyMat ๐
) |
11 |
|
cpmidgsum.k |
โข ๐พ = ( ๐ถ โ ๐ ) |
12 |
|
cpmidgsum.h |
โข ๐ป = ( ๐พ ยท 1 ) |
13 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
14 |
10 1 2 3 13
|
chpmatply1 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ถ โ ๐ ) โ ( Base โ ๐ ) ) |
15 |
11 14
|
eqeltrid |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐พ โ ( Base โ ๐ ) ) |
16 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
17 |
|
eqid |
โข ( ๐ matToPolyMat ๐
) = ( ๐ matToPolyMat ๐
) |
18 |
|
eqid |
โข ( Base โ ๐
) = ( Base โ ๐
) |
19 |
3 4 16 7 6 5 17 1 2 9 18 13 9 8 12
|
pmatcollpwscmat |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐พ โ ( Base โ ๐ ) ) โ ๐ป = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) ) |
20 |
15 19
|
syld3an3 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐ป = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) ) |