Step |
Hyp |
Ref |
Expression |
1 |
|
chcoeffeq.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
chcoeffeq.b |
โข ๐ต = ( Base โ ๐ด ) |
3 |
|
chcoeffeq.p |
โข ๐ = ( Poly1 โ ๐
) |
4 |
|
chcoeffeq.y |
โข ๐ = ( ๐ Mat ๐ ) |
5 |
|
chcoeffeq.r |
โข ร = ( .r โ ๐ ) |
6 |
|
chcoeffeq.s |
โข โ = ( -g โ ๐ ) |
7 |
|
chcoeffeq.0 |
โข 0 = ( 0g โ ๐ ) |
8 |
|
chcoeffeq.t |
โข ๐ = ( ๐ matToPolyMat ๐
) |
9 |
|
chcoeffeq.c |
โข ๐ถ = ( ๐ CharPlyMat ๐
) |
10 |
|
chcoeffeq.k |
โข ๐พ = ( ๐ถ โ ๐ ) |
11 |
|
chcoeffeq.g |
โข ๐บ = ( ๐ โ โ0 โฆ if ( ๐ = 0 , ( 0 โ ( ( ๐ โ ๐ ) ร ( ๐ โ ( ๐ โ 0 ) ) ) ) , if ( ๐ = ( ๐ + 1 ) , ( ๐ โ ( ๐ โ ๐ ) ) , if ( ( ๐ + 1 ) < ๐ , 0 , ( ( ๐ โ ( ๐ โ ( ๐ โ 1 ) ) ) โ ( ( ๐ โ ๐ ) ร ( ๐ โ ( ๐ โ ๐ ) ) ) ) ) ) ) ) |
12 |
|
chcoeffeq.w |
โข ๐ = ( Base โ ๐ ) |
13 |
|
chcoeffeq.1 |
โข 1 = ( 1r โ ๐ด ) |
14 |
|
chcoeffeq.m |
โข โ = ( ยท๐ โ ๐ด ) |
15 |
|
chcoeffeq.u |
โข ๐ = ( ๐ cPolyMatToMat ๐
) |
16 |
|
eqid |
โข ( ๐ ConstPolyMat ๐
) = ( ๐ ConstPolyMat ๐
) |
17 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
18 |
|
eqid |
โข ( 1r โ ๐ ) = ( 1r โ ๐ ) |
19 |
|
eqid |
โข ( var1 โ ๐
) = ( var1 โ ๐
) |
20 |
|
eqid |
โข ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) = ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) |
21 |
|
eqid |
โข ( ๐ maAdju ๐ ) = ( ๐ maAdju ๐ ) |
22 |
|
eqid |
โข ( Poly1 โ ๐ด ) = ( Poly1 โ ๐ด ) |
23 |
|
eqid |
โข ( var1 โ ๐ด ) = ( var1 โ ๐ด ) |
24 |
|
eqid |
โข ( ยท๐ โ ( Poly1 โ ๐ด ) ) = ( ยท๐ โ ( Poly1 โ ๐ด ) ) |
25 |
|
eqid |
โข ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) = ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) |
26 |
|
eqid |
โข ( ๐ pMatToMatPoly ๐
) = ( ๐ pMatToMatPoly ๐
) |
27 |
1 2 3 4 8 5 6 7 11 16 17 18 19 20 21 12 22 23 24 25 15 26
|
cpmadumatpoly |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ โ ๐ โ โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) |
28 |
|
eqid |
โข ( .g โ ( mulGrp โ ๐ ) ) = ( .g โ ( mulGrp โ ๐ ) ) |
29 |
|
eqid |
โข ( algSc โ ๐ ) = ( algSc โ ๐ ) |
30 |
|
eqid |
โข ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) |
31 |
1 2 3 4 19 28 17 18 29 9 10 30 13 14 8 12 22 23 24 25 26
|
cpmidpmat |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) |
32 |
|
eqid |
โข ( ๐ CharPlyMat ๐
) = ( ๐ CharPlyMat ๐
) |
33 |
1 2 32 3 4 19 8 6 17 18 20 21 5
|
cpmadurid |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) = ( ( ( ๐ CharPlyMat ๐
) โ ๐ ) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) |
34 |
9
|
fveq1i |
โข ( ๐ถ โ ๐ ) = ( ( ๐ CharPlyMat ๐
) โ ๐ ) |
35 |
10 34
|
eqtri |
โข ๐พ = ( ( ๐ CharPlyMat ๐
) โ ๐ ) |
36 |
35
|
a1i |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐พ = ( ( ๐ CharPlyMat ๐
) โ ๐ ) ) |
37 |
36
|
eqcomd |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ๐ CharPlyMat ๐
) โ ๐ ) = ๐พ ) |
38 |
37
|
oveq1d |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ( ๐ CharPlyMat ๐
) โ ๐ ) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) |
39 |
33 38
|
eqtrd |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) |
40 |
|
fveq2 |
โข ( ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) ) |
41 |
|
simpr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) |
42 |
41
|
adantr |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) |
43 |
|
simpr |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) |
44 |
42 43
|
eqeq12d |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) โ ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) ) |
45 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
|
chcoeffeqlem |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ( ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
46 |
45
|
adantr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
47 |
46
|
adantr |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
48 |
44 47
|
sylbid |
โข ( ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โง ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
49 |
48
|
exp31 |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) ) ) |
50 |
49
|
com24 |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) ) ) |
51 |
40 50
|
syl5 |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ( ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) ) ) |
52 |
51
|
ex |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) ) ) ) |
53 |
52
|
com24 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ ( ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) = ( ๐พ ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) ) ) ) |
54 |
31 39 53
|
mp2d |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) ) |
55 |
54
|
impl |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
56 |
55
|
reximdva |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โ ( โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
57 |
56
|
reximdva |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( โ ๐ โ โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ( ( ๐ pMatToMatPoly ๐
) โ ( ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ร ( ( ๐ maAdju ๐ ) โ ( ( ( var1 โ ๐
) ( ยท๐ โ ๐ ) ( 1r โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) ) ) = ( ( Poly1 โ ๐ด ) ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ( ๐บ โ ๐ ) ) ( ยท๐ โ ( Poly1 โ ๐ด ) ) ( ๐ ( .g โ ( mulGrp โ ( Poly1 โ ๐ด ) ) ) ( var1 โ ๐ด ) ) ) ) ) โ โ ๐ โ โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) ) |
58 |
27 57
|
mpd |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ โ ๐ โ โ โ ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) โ ๐ โ โ0 ( ๐ โ ( ๐บ โ ๐ ) ) = ( ( ( coe1 โ ๐พ ) โ ๐ ) โ 1 ) ) |