Step | Hyp | Ref
| Expression |
1 | | 0fin 9121 |
. . 3
โข โ
โ Fin |
2 | | id 22 |
. . 3
โข (๐
โ Ring โ ๐
โ Ring) |
3 | | 0ex 5268 |
. . . . 5
โข โ
โ V |
4 | 3 | snid 4626 |
. . . 4
โข โ
โ {โ
} |
5 | | mat0dimbas0 21838 |
. . . 4
โข (๐
โ Ring โ
(Baseโ(โ
Mat ๐
)) = {โ
}) |
6 | 4, 5 | eleqtrrid 2841 |
. . 3
โข (๐
โ Ring โ โ
โ (Baseโ(โ
Mat ๐
))) |
7 | | chpmat0.c |
. . . 4
โข ๐ถ = (โ
CharPlyMat ๐
) |
8 | | eqid 2733 |
. . . 4
โข (โ
Mat ๐
) = (โ
Mat ๐
) |
9 | | eqid 2733 |
. . . 4
โข
(Baseโ(โ
Mat ๐
)) = (Baseโ(โ
Mat ๐
)) |
10 | | eqid 2733 |
. . . 4
โข
(Poly1โ๐
) = (Poly1โ๐
) |
11 | | eqid 2733 |
. . . 4
โข (โ
Mat (Poly1โ๐
)) = (โ
Mat
(Poly1โ๐
)) |
12 | | eqid 2733 |
. . . 4
โข (โ
maDet (Poly1โ๐
)) = (โ
maDet
(Poly1โ๐
)) |
13 | | eqid 2733 |
. . . 4
โข
(-gโ(โ
Mat (Poly1โ๐
))) =
(-gโ(โ
Mat (Poly1โ๐
))) |
14 | | eqid 2733 |
. . . 4
โข
(var1โ๐
) = (var1โ๐
) |
15 | | eqid 2733 |
. . . 4
โข (
ยท๐ โ(โ
Mat
(Poly1โ๐
))) = ( ยท๐
โ(โ
Mat (Poly1โ๐
))) |
16 | | eqid 2733 |
. . . 4
โข (โ
matToPolyMat ๐
) = (โ
matToPolyMat ๐
) |
17 | | eqid 2733 |
. . . 4
โข
(1rโ(โ
Mat (Poly1โ๐
))) =
(1rโ(โ
Mat (Poly1โ๐
))) |
18 | 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 | chpmatval 22203 |
. . 3
โข ((โ
โ Fin โง ๐
โ
Ring โง โ
โ (Baseโ(โ
Mat ๐
))) โ (๐ถโโ
) = ((โ
maDet
(Poly1โ๐
))โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
)))) |
19 | 1, 2, 6, 18 | mp3an2i 1467 |
. 2
โข (๐
โ Ring โ (๐ถโโ
) = ((โ
maDet (Poly1โ๐
))โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
)))) |
20 | 10 | ply1ring 21642 |
. . . 4
โข (๐
โ Ring โ
(Poly1โ๐
)
โ Ring) |
21 | | mdet0pr 21964 |
. . . . 5
โข
((Poly1โ๐
) โ Ring โ (โ
maDet
(Poly1โ๐
))
= {โจโ
, (1rโ(Poly1โ๐
))โฉ}) |
22 | 21 | fveq1d 6848 |
. . . 4
โข
((Poly1โ๐
) โ Ring โ ((โ
maDet
(Poly1โ๐
))โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
))) = ({โจโ
,
(1rโ(Poly1โ๐
))โฉ}โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
)))) |
23 | 20, 22 | syl 17 |
. . 3
โข (๐
โ Ring โ ((โ
maDet (Poly1โ๐
))โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
))) = ({โจโ
,
(1rโ(Poly1โ๐
))โฉ}โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
)))) |
24 | 11 | mat0dimid 21840 |
. . . . . . . . . 10
โข
((Poly1โ๐
) โ Ring โ
(1rโ(โ
Mat (Poly1โ๐
))) = โ
) |
25 | 20, 24 | syl 17 |
. . . . . . . . 9
โข (๐
โ Ring โ
(1rโ(โ
Mat (Poly1โ๐
))) = โ
) |
26 | 25 | oveq2d 7377 |
. . . . . . . 8
โข (๐
โ Ring โ
((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
)))) = ((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))โ
)) |
27 | | eqid 2733 |
. . . . . . . . . 10
โข
(Baseโ(Poly1โ๐
)) =
(Baseโ(Poly1โ๐
)) |
28 | 14, 10, 27 | vr1cl 21611 |
. . . . . . . . 9
โข (๐
โ Ring โ
(var1โ๐
)
โ (Baseโ(Poly1โ๐
))) |
29 | 11 | mat0dimscm 21841 |
. . . . . . . . 9
โข
(((Poly1โ๐
) โ Ring โง
(var1โ๐
)
โ (Baseโ(Poly1โ๐
))) โ ((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))โ
) = โ
) |
30 | 20, 28, 29 | syl2anc 585 |
. . . . . . . 8
โข (๐
โ Ring โ
((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))โ
) = โ
) |
31 | 26, 30 | eqtrd 2773 |
. . . . . . 7
โข (๐
โ Ring โ
((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
)))) = โ
) |
32 | | d0mat2pmat 22110 |
. . . . . . 7
โข (๐
โ Ring โ ((โ
matToPolyMat ๐
)โโ
) = โ
) |
33 | 31, 32 | oveq12d 7379 |
. . . . . 6
โข (๐
โ Ring โ
(((var1โ๐
)( ยท๐
โ(โ
Mat (Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
)) =
(โ
(-gโ(โ
Mat (Poly1โ๐
)))โ
)) |
34 | 11 | matring 21815 |
. . . . . . . . 9
โข ((โ
โ Fin โง (Poly1โ๐
) โ Ring) โ (โ
Mat
(Poly1โ๐
))
โ Ring) |
35 | 1, 20, 34 | sylancr 588 |
. . . . . . . 8
โข (๐
โ Ring โ (โ
Mat
(Poly1โ๐
))
โ Ring) |
36 | | ringgrp 19977 |
. . . . . . . 8
โข ((โ
Mat (Poly1โ๐
)) โ Ring โ (โ
Mat
(Poly1โ๐
))
โ Grp) |
37 | 35, 36 | syl 17 |
. . . . . . 7
โข (๐
โ Ring โ (โ
Mat
(Poly1โ๐
))
โ Grp) |
38 | | mat0dimbas0 21838 |
. . . . . . . . 9
โข
((Poly1โ๐
) โ Ring โ (Baseโ(โ
Mat (Poly1โ๐
))) = {โ
}) |
39 | 20, 38 | syl 17 |
. . . . . . . 8
โข (๐
โ Ring โ
(Baseโ(โ
Mat (Poly1โ๐
))) = {โ
}) |
40 | 4, 39 | eleqtrrid 2841 |
. . . . . . 7
โข (๐
โ Ring โ โ
โ (Baseโ(โ
Mat (Poly1โ๐
)))) |
41 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ(โ
Mat (Poly1โ๐
))) = (Baseโ(โ
Mat
(Poly1โ๐
))) |
42 | | eqid 2733 |
. . . . . . . 8
โข
(0gโ(โ
Mat (Poly1โ๐
))) =
(0gโ(โ
Mat (Poly1โ๐
))) |
43 | 41, 42, 13 | grpsubid 18839 |
. . . . . . 7
โข
(((โ
Mat (Poly1โ๐
)) โ Grp โง โ
โ
(Baseโ(โ
Mat (Poly1โ๐
)))) โ
(โ
(-gโ(โ
Mat (Poly1โ๐
)))โ
) =
(0gโ(โ
Mat (Poly1โ๐
)))) |
44 | 37, 40, 43 | syl2anc 585 |
. . . . . 6
โข (๐
โ Ring โ
(โ
(-gโ(โ
Mat (Poly1โ๐
)))โ
) =
(0gโ(โ
Mat (Poly1โ๐
)))) |
45 | 33, 44 | eqtrd 2773 |
. . . . 5
โข (๐
โ Ring โ
(((var1โ๐
)( ยท๐
โ(โ
Mat (Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
)) =
(0gโ(โ
Mat (Poly1โ๐
)))) |
46 | 45 | fveq2d 6850 |
. . . 4
โข (๐
โ Ring โ
({โจโ
, (1rโ(Poly1โ๐
))โฉ}โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
))) = ({โจโ
,
(1rโ(Poly1โ๐
))โฉ}โ(0gโ(โ
Mat (Poly1โ๐
))))) |
47 | 11 | mat0dim0 21839 |
. . . . . . 7
โข
((Poly1โ๐
) โ Ring โ
(0gโ(โ
Mat (Poly1โ๐
))) = โ
) |
48 | 20, 47 | syl 17 |
. . . . . 6
โข (๐
โ Ring โ
(0gโ(โ
Mat (Poly1โ๐
))) = โ
) |
49 | 48 | fveq2d 6850 |
. . . . 5
โข (๐
โ Ring โ
({โจโ
, (1rโ(Poly1โ๐
))โฉ}โ(0gโ(โ
Mat (Poly1โ๐
)))) = ({โจโ
,
(1rโ(Poly1โ๐
))โฉ}โโ
)) |
50 | | fvex 6859 |
. . . . . 6
โข
(1rโ(Poly1โ๐
)) โ V |
51 | 3, 50 | fvsn 7131 |
. . . . 5
โข
({โจโ
, (1rโ(Poly1โ๐
))โฉ}โโ
) =
(1rโ(Poly1โ๐
)) |
52 | 49, 51 | eqtrdi 2789 |
. . . 4
โข (๐
โ Ring โ
({โจโ
, (1rโ(Poly1โ๐
))โฉ}โ(0gโ(โ
Mat (Poly1โ๐
)))) =
(1rโ(Poly1โ๐
))) |
53 | 46, 52 | eqtrd 2773 |
. . 3
โข (๐
โ Ring โ
({โจโ
, (1rโ(Poly1โ๐
))โฉ}โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
))) =
(1rโ(Poly1โ๐
))) |
54 | 23, 53 | eqtrd 2773 |
. 2
โข (๐
โ Ring โ ((โ
maDet (Poly1โ๐
))โ(((var1โ๐
)(
ยท๐ โ(โ
Mat
(Poly1โ๐
)))(1rโ(โ
Mat
(Poly1โ๐
))))(-gโ(โ
Mat
(Poly1โ๐
)))((โ
matToPolyMat ๐
)โโ
))) =
(1rโ(Poly1โ๐
))) |
55 | 19, 54 | eqtrd 2773 |
1
โข (๐
โ Ring โ (๐ถโโ
) =
(1rโ(Poly1โ๐
))) |