Step |
Hyp |
Ref |
Expression |
1 |
|
cpmadugsum.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
cpmadugsum.b |
โข ๐ต = ( Base โ ๐ด ) |
3 |
|
cpmadugsum.p |
โข ๐ = ( Poly1 โ ๐
) |
4 |
|
cpmadugsum.y |
โข ๐ = ( ๐ Mat ๐ ) |
5 |
|
cpmadugsum.t |
โข ๐ = ( ๐ matToPolyMat ๐
) |
6 |
|
cpmadugsum.x |
โข ๐ = ( var1 โ ๐
) |
7 |
|
cpmadugsum.e |
โข โ = ( .g โ ( mulGrp โ ๐ ) ) |
8 |
|
cpmadugsum.m |
โข ยท = ( ยท๐ โ ๐ ) |
9 |
|
cpmadugsum.r |
โข ร = ( .r โ ๐ ) |
10 |
|
cpmadugsum.1 |
โข 1 = ( 1r โ ๐ ) |
11 |
|
cpmadugsum.g |
โข + = ( +g โ ๐ ) |
12 |
|
cpmadugsum.s |
โข โ = ( -g โ ๐ ) |
13 |
|
cpmadugsum.i |
โข ๐ผ = ( ( ๐ ยท 1 ) โ ( ๐ โ ๐ ) ) |
14 |
|
cpmadugsum.j |
โข ๐ฝ = ( ๐ maAdju ๐ ) |
15 |
|
cpmadugsum.0 |
โข 0 = ( 0g โ ๐ ) |
16 |
|
cpmadugsum.g2 |
โข ๐บ = ( ๐ โ โ0 โฆ if ( ๐ = 0 , ( 0 โ ( ( ๐ โ ๐ ) ร ( ๐ โ ( ๐ โ 0 ) ) ) ) , if ( ๐ = ( ๐ + 1 ) , ( ๐ โ ( ๐ โ ๐ ) ) , if ( ( ๐ + 1 ) < ๐ , 0 , ( ( ๐ โ ( ๐ โ ( ๐ โ 1 ) ) ) โ ( ( ๐ โ ๐ ) ร ( ๐ โ ( ๐ โ ๐ ) ) ) ) ) ) ) ) |
17 |
|
cpmidgsum2.c |
โข ๐ถ = ( ๐ CharPlyMat ๐
) |
18 |
|
cpmidgsum2.k |
โข ๐พ = ( ๐ถ โ ๐ ) |
19 |
|
cpmidg2sum.u |
โข ๐ = ( algSc โ ๐ ) |
20 |
|
eqid |
โข ( ๐พ ยท 1 ) = ( ๐พ ยท 1 ) |
21 |
1 2 3 4 6 7 8 10 19 17 18 20
|
cpmidgsum |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐พ ยท 1 ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) ) |
22 |
21
|
eqcomd |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) = ( ๐พ ยท 1 ) ) |
23 |
22
|
ad3antrrr |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โง ( ๐พ ยท 1 ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) โ ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) = ( ๐พ ยท 1 ) ) |
24 |
|
simpr |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โง ( ๐พ ยท 1 ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) โ ( ๐พ ยท 1 ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) |
25 |
23 24
|
eqtrd |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โง ( ๐พ ยท 1 ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) โ ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) |
26 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 20
|
cpmidgsum2 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ โ ๐ โ โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ( ๐พ ยท 1 ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) |
27 |
25 26
|
reximddv2 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ โ ๐ โ โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐บ โ ๐ ) ) ) ) ) |