Step |
Hyp |
Ref |
Expression |
1 |
|
cpmadumatpoly.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
cpmadumatpoly.b |
โข ๐ต = ( Base โ ๐ด ) |
3 |
|
cpmadumatpoly.p |
โข ๐ = ( Poly1 โ ๐
) |
4 |
|
cpmadumatpoly.y |
โข ๐ = ( ๐ Mat ๐ ) |
5 |
|
cpmadumatpoly.t |
โข ๐ = ( ๐ matToPolyMat ๐
) |
6 |
|
cpmadumatpoly.r |
โข ร = ( .r โ ๐ ) |
7 |
|
cpmadumatpoly.m0 |
โข โ = ( -g โ ๐ ) |
8 |
|
cpmadumatpoly.0 |
โข 0 = ( 0g โ ๐ ) |
9 |
|
cpmadumatpoly.g |
โข ๐บ = ( ๐ โ โ0 โฆ if ( ๐ = 0 , ( 0 โ ( ( ๐ โ ๐ ) ร ( ๐ โ ( ๐ โ 0 ) ) ) ) , if ( ๐ = ( ๐ + 1 ) , ( ๐ โ ( ๐ โ ๐ ) ) , if ( ( ๐ + 1 ) < ๐ , 0 , ( ( ๐ โ ( ๐ โ ( ๐ โ 1 ) ) ) โ ( ( ๐ โ ๐ ) ร ( ๐ โ ( ๐ โ ๐ ) ) ) ) ) ) ) ) |
10 |
|
cpmadumatpoly.s |
โข ๐ = ( ๐ ConstPolyMat ๐
) |
11 |
|
cpmadumatpoly.m1 |
โข ยท = ( ยท๐ โ ๐ ) |
12 |
|
cpmadumatpoly.1 |
โข 1 = ( 1r โ ๐ ) |
13 |
|
cpmadumatpoly.z |
โข ๐ = ( var1 โ ๐
) |
14 |
|
cpmadumatpoly.d |
โข ๐ท = ( ( ๐ ยท 1 ) โ ( ๐ โ ๐ ) ) |
15 |
|
cpmadumatpoly.j |
โข ๐ฝ = ( ๐ maAdju ๐ ) |
16 |
|
cpmadumatpoly.w |
โข ๐ = ( Base โ ๐ ) |
17 |
|
cpmadumatpoly.q |
โข ๐ = ( Poly1 โ ๐ด ) |
18 |
|
cpmadumatpoly.x |
โข ๐ = ( var1 โ ๐ด ) |
19 |
|
cpmadumatpoly.m2 |
โข โ = ( ยท๐ โ ๐ ) |
20 |
|
cpmadumatpoly.e |
โข โ = ( .g โ ( mulGrp โ ๐ ) ) |
21 |
|
cpmadumatpoly.u |
โข ๐ = ( ๐ cPolyMatToMat ๐
) |
22 |
|
fvexd |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( 0g โ ๐ด ) โ V ) |
23 |
|
crngring |
โข ( ๐
โ CRing โ ๐
โ Ring ) |
24 |
23
|
anim2i |
โข ( ( ๐ โ Fin โง ๐
โ CRing ) โ ( ๐ โ Fin โง ๐
โ Ring ) ) |
25 |
24
|
3adant3 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ โ Fin โง ๐
โ Ring ) ) |
26 |
25
|
ad2antrr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ๐ โ Fin โง ๐
โ Ring ) ) |
27 |
10 3 4
|
0elcpmat |
โข ( ( ๐ โ Fin โง ๐
โ Ring ) โ ( 0g โ ๐ ) โ ๐ ) |
28 |
26 27
|
syl |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( 0g โ ๐ ) โ ๐ ) |
29 |
1 2 3 4 6 7 8 5 9 10
|
chfacfisfcpmat |
โข ( ( ( ๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ๐บ : โ0 โถ ๐ ) |
30 |
23 29
|
syl3anl2 |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ๐บ : โ0 โถ ๐ ) |
31 |
30
|
anassrs |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ๐บ : โ0 โถ ๐ ) |
32 |
1 2 10 21
|
cpm2mf |
โข ( ( ๐ โ Fin โง ๐
โ Ring ) โ ๐ : ๐ โถ ๐ต ) |
33 |
26 32
|
syl |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ๐ : ๐ โถ ๐ต ) |
34 |
|
ssidd |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ๐ โ ๐ ) |
35 |
|
nn0ex |
โข โ0 โ V |
36 |
35
|
a1i |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ โ0 โ V ) |
37 |
10
|
ovexi |
โข ๐ โ V |
38 |
37
|
a1i |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ๐ โ V ) |
39 |
1 2 3 4 6 7 8 5 9
|
chfacffsupp |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ( ๐ โ โ โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) ) โ ๐บ finSupp ( 0g โ ๐ ) ) |
40 |
39
|
anassrs |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ๐บ finSupp ( 0g โ ๐ ) ) |
41 |
|
eqid |
โข ( 0g โ ๐ด ) = ( 0g โ ๐ด ) |
42 |
|
eqid |
โข ( 0g โ ๐ ) = ( 0g โ ๐ ) |
43 |
1 21 3 4 41 42
|
m2cpminv0 |
โข ( ( ๐ โ Fin โง ๐
โ Ring ) โ ( ๐ โ ( 0g โ ๐ ) ) = ( 0g โ ๐ด ) ) |
44 |
23 43
|
sylan2 |
โข ( ( ๐ โ Fin โง ๐
โ CRing ) โ ( ๐ โ ( 0g โ ๐ ) ) = ( 0g โ ๐ด ) ) |
45 |
44
|
3adant3 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ โ ( 0g โ ๐ ) ) = ( 0g โ ๐ด ) ) |
46 |
45
|
ad2antrr |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ๐ โ ( 0g โ ๐ ) ) = ( 0g โ ๐ด ) ) |
47 |
22 28 31 33 34 36 38 40 46
|
fsuppcor |
โข ( ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ ) โง ๐ โ ( ๐ต โm ( 0 ... ๐ ) ) ) โ ( ๐ โ ๐บ ) finSupp ( 0g โ ๐ด ) ) |