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 |
|
cpmidgsumm2pm.o |
โข ๐ = ( 1r โ ๐ด ) |
14 |
|
cpmidgsumm2pm.m |
โข โ = ( ยท๐ โ ๐ด ) |
15 |
|
cpmidgsumm2pm.t |
โข ๐ = ( ๐ matToPolyMat ๐
) |
16 |
1 2 3 4 5 6 7 8 9 10 11 12
|
cpmidgsum |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐ป = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) ) |
17 |
|
3simpa |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ โ Fin โง ๐
โ CRing ) ) |
18 |
17
|
adantr |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ๐ โ Fin โง ๐
โ CRing ) ) |
19 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
20 |
10 1 2 3 19
|
chpmatply1 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ถ โ ๐ ) โ ( Base โ ๐ ) ) |
21 |
11 20
|
eqeltrid |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐พ โ ( Base โ ๐ ) ) |
22 |
|
eqid |
โข ( coe1 โ ๐พ ) = ( coe1 โ ๐พ ) |
23 |
|
eqid |
โข ( Base โ ๐
) = ( Base โ ๐
) |
24 |
22 19 3 23
|
coe1fvalcl |
โข ( ( ๐พ โ ( Base โ ๐ ) โง ๐ โ โ0 ) โ ( ( coe1 โ ๐พ ) โ ๐ ) โ ( Base โ ๐
) ) |
25 |
21 24
|
sylan |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ( coe1 โ ๐พ ) โ ๐ ) โ ( Base โ ๐
) ) |
26 |
|
crngring |
โข ( ๐
โ CRing โ ๐
โ Ring ) |
27 |
26
|
anim2i |
โข ( ( ๐ โ Fin โง ๐
โ CRing ) โ ( ๐ โ Fin โง ๐
โ Ring ) ) |
28 |
1
|
matring |
โข ( ( ๐ โ Fin โง ๐
โ Ring ) โ ๐ด โ Ring ) |
29 |
2 13
|
ringidcl |
โข ( ๐ด โ Ring โ ๐ โ ๐ต ) |
30 |
27 28 29
|
3syl |
โข ( ( ๐ โ Fin โง ๐
โ CRing ) โ ๐ โ ๐ต ) |
31 |
30
|
3adant3 |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
32 |
31
|
adantr |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ๐ โ ๐ต ) |
33 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
34 |
15 1 2 3 4 33 23 9 14 7
|
mat2pmatlin |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing ) โง ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ( Base โ ๐
) โง ๐ โ ๐ต ) ) โ ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) = ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท ( ๐ โ ๐ ) ) ) |
35 |
18 25 32 34
|
syl12anc |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) = ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท ( ๐ โ ๐ ) ) ) |
36 |
15 1 2 3 4 33
|
mat2pmatrhm |
โข ( ( ๐ โ Fin โง ๐
โ CRing ) โ ๐ โ ( ๐ด RingHom ๐ ) ) |
37 |
13 8
|
rhm1 |
โข ( ๐ โ ( ๐ด RingHom ๐ ) โ ( ๐ โ ๐ ) = 1 ) |
38 |
17 36 37
|
3syl |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ โ ๐ ) = 1 ) |
39 |
38
|
adantr |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ๐ โ ๐ ) = 1 ) |
40 |
39
|
oveq2d |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท ( ๐ โ ๐ ) ) = ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) |
41 |
35 40
|
eqtr2d |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) = ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) ) |
42 |
41
|
oveq2d |
โข ( ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โง ๐ โ โ0 ) โ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) = ( ( ๐ โ ๐ ) ยท ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) ) ) |
43 |
42
|
mpteq2dva |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) ) ) ) |
44 |
43
|
oveq2d |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ( ๐ โ ( ( coe1 โ ๐พ ) โ ๐ ) ) ยท 1 ) ) ) ) = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) ) ) ) ) |
45 |
16 44
|
eqtrd |
โข ( ( ๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต ) โ ๐ป = ( ๐ ฮฃg ( ๐ โ โ0 โฆ ( ( ๐ โ ๐ ) ยท ( ๐ โ ( ( ( coe1 โ ๐พ ) โ ๐ ) โ ๐ ) ) ) ) ) ) |