Step | Hyp | Ref
| Expression |
1 | | cayleyhamilton.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
2 | | cayleyhamilton.b |
. . . 4
โข ๐ต = (Baseโ๐ด) |
3 | | eqid 2733 |
. . . 4
โข
(Poly1โ๐
) = (Poly1โ๐
) |
4 | | eqid 2733 |
. . . 4
โข (๐ Mat
(Poly1โ๐
))
= (๐ Mat
(Poly1โ๐
)) |
5 | | eqid 2733 |
. . . 4
โข
(.rโ(๐ Mat (Poly1โ๐
))) =
(.rโ(๐ Mat
(Poly1โ๐
))) |
6 | | eqid 2733 |
. . . 4
โข
(-gโ(๐ Mat (Poly1โ๐
))) =
(-gโ(๐ Mat
(Poly1โ๐
))) |
7 | | eqid 2733 |
. . . 4
โข
(0gโ(๐ Mat (Poly1โ๐
))) =
(0gโ(๐ Mat
(Poly1โ๐
))) |
8 | | eqid 2733 |
. . . 4
โข (๐ matToPolyMat ๐
) = (๐ matToPolyMat ๐
) |
9 | | cayleyhamilton.c |
. . . 4
โข ๐ถ = (๐ CharPlyMat ๐
) |
10 | | eqid 2733 |
. . . 4
โข (๐ถโ๐) = (๐ถโ๐) |
11 | | eqeq1 2737 |
. . . . . 6
โข (๐ = ๐ โ (๐ = 0 โ ๐ = 0)) |
12 | | eqeq1 2737 |
. . . . . . 7
โข (๐ = ๐ โ (๐ = (๐ + 1) โ ๐ = (๐ + 1))) |
13 | | breq2 5113 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ + 1) < ๐ โ (๐ + 1) < ๐)) |
14 | | oveq1 7368 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
15 | 14 | fveq2d 6850 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ(๐ โ 1)) = (๐โ(๐ โ 1))) |
16 | 15 | fveq2d 6850 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1))) = ((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))) |
17 | | fveq2 6846 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
18 | 17 | fveq2d 6850 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ matToPolyMat ๐
)โ(๐โ๐)) = ((๐ matToPolyMat ๐
)โ(๐โ๐))) |
19 | 18 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ = ๐ โ (((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))) = (((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))) |
20 | 16, 19 | oveq12d 7379 |
. . . . . . . 8
โข (๐ = ๐ โ (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))) = (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))) |
21 | 13, 20 | ifbieq2d 4516 |
. . . . . . 7
โข (๐ = ๐ โ if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))) = if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))))) |
22 | 12, 21 | ifbieq2d 4516 |
. . . . . 6
โข (๐ = ๐ โ if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))))) = if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))) |
23 | 11, 22 | ifbieq2d 4516 |
. . . . 5
โข (๐ = ๐ โ if(๐ = 0, ((0gโ(๐ Mat
(Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))) = if(๐ = 0, ((0gโ(๐ Mat
(Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))))))) |
24 | 23 | cbvmptv 5222 |
. . . 4
โข (๐ โ โ0
โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))))))) = (๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐)))))))) |
25 | | eqid 2733 |
. . . 4
โข
(Baseโ(๐ Mat
(Poly1โ๐
))) = (Baseโ(๐ Mat (Poly1โ๐
))) |
26 | | eqid 2733 |
. . . 4
โข
(1rโ๐ด) = (1rโ๐ด) |
27 | | cayleyhamilton.m |
. . . 4
โข โ = (
ยท๐ โ๐ด) |
28 | | eqid 2733 |
. . . 4
โข (๐ cPolyMatToMat ๐
) = (๐ cPolyMatToMat ๐
) |
29 | | cayleyhamilton.e |
. . . 4
โข โ =
(.gโ(mulGrpโ๐ด)) |
30 | | eqid 2733 |
. . . 4
โข
(.gโ(mulGrpโ(๐ Mat (Poly1โ๐
)))) =
(.gโ(mulGrpโ(๐ Mat (Poly1โ๐
)))) |
31 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
24, 25, 26, 27, 28, 29, 30 | cayhamlem4 22260 |
. . 3
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ cPolyMatToMat ๐
)โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) |
32 | | eqid 2733 |
. . . . . . . . 9
โข (๐ ConstPolyMat ๐
) = (๐ ConstPolyMat ๐
) |
33 | 28, 32 | cpm2mfval 22121 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ CRing) โ (๐ cPolyMatToMat ๐
) = (๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))) |
34 | 33 | eqcomd 2739 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ CRing) โ (๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0))) = (๐ cPolyMatToMat ๐
)) |
35 | 34 | 3adant3 1133 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0))) = (๐ cPolyMatToMat ๐
)) |
36 | 35 | fveq1d 6848 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) = ((๐ cPolyMatToMat ๐
)โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) |
37 | 36 | eqeq2d 2744 |
. . . 4
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ ((๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ cPolyMatToMat ๐
)โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))))) |
38 | 37 | 2rexbidv 3210 |
. . 3
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ cPolyMatToMat ๐
)โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))))) |
39 | 31, 38 | mpbird 257 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) |
40 | | cayleyhamilton.k |
. . . . . . . . . . . . 13
โข ๐พ = (coe1โ(๐ถโ๐)) |
41 | 40 | eqcomi 2742 |
. . . . . . . . . . . 12
โข
(coe1โ(๐ถโ๐)) = ๐พ |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ
(coe1โ(๐ถโ๐)) = ๐พ) |
43 | 42 | fveq1d 6848 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ
((coe1โ(๐ถโ๐))โ๐) = (๐พโ๐)) |
44 | 43 | oveq1d 7376 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ
(((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)) = ((๐พโ๐) โ (๐ โ ๐))) |
45 | 44 | mpteq2dva 5209 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ โ โ0 โฆ
(((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐))) = (๐ โ โ0 โฆ ((๐พโ๐) โ (๐ โ ๐)))) |
46 | 45 | oveq2d 7377 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐))))) |
47 | 46 | eqeq1d 2735 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))))) |
48 | 47 | biimpa 478 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) |
49 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐)) = (๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))) |
50 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐) = ((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)) |
51 | 49, 50 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)) = ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))) |
52 | 51 | cbvmptv 5222 |
. . . . . . . . . 10
โข (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))) = (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))) |
53 | 52 | oveq2i 7372 |
. . . . . . . . 9
โข ((๐ Mat
(Poly1โ๐
))
ฮฃg (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) = ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) |
54 | 53 | a1i 11 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) = ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) |
55 | 1, 2, 3, 4, 5, 6, 7, 8, 24, 30 | cayhamlem1 22238 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) = (0gโ(๐ Mat
(Poly1โ๐
)))) |
56 | 54, 55 | eqtrd 2773 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) = (0gโ(๐ Mat
(Poly1โ๐
)))) |
57 | | fveq2 6846 |
. . . . . . . 8
โข (((๐ Mat
(Poly1โ๐
))
ฮฃg (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) = (0gโ(๐ Mat
(Poly1โ๐
))) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ(0gโ(๐ Mat (Poly1โ๐
))))) |
58 | | crngring 19984 |
. . . . . . . . . . . . 13
โข (๐
โ CRing โ ๐
โ Ring) |
59 | 58 | anim2i 618 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ CRing) โ (๐ โ Fin โง ๐
โ Ring)) |
60 | 59 | 3adant3 1133 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐
โ Ring)) |
61 | 28, 32 | cpm2mfval 22121 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ cPolyMatToMat ๐
) = (๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))) |
62 | 61 | eqcomd 2739 |
. . . . . . . . . . . . 13
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0))) = (๐ cPolyMatToMat ๐
)) |
63 | 62 | fveq1d 6848 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ(0gโ(๐ Mat (Poly1โ๐
)))) = ((๐ cPolyMatToMat ๐
)โ(0gโ(๐ Mat (Poly1โ๐
))))) |
64 | | eqid 2733 |
. . . . . . . . . . . . 13
โข
(0gโ๐ด) = (0gโ๐ด) |
65 | 1, 28, 3, 4, 64, 7 | m2cpminv0 22133 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ ((๐ cPolyMatToMat ๐
)โ(0gโ(๐ Mat
(Poly1โ๐
)))) = (0gโ๐ด)) |
66 | 63, 65 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ(0gโ(๐ Mat (Poly1โ๐
)))) = (0gโ๐ด)) |
67 | 60, 66 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ(0gโ(๐ Mat (Poly1โ๐
)))) = (0gโ๐ด)) |
68 | | cayleyhamilton.0 |
. . . . . . . . . 10
โข 0 =
(0gโ๐ด) |
69 | 67, 68 | eqtr4di 2791 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ(0gโ(๐ Mat (Poly1โ๐
)))) = 0 ) |
70 | 69 | adantr 482 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ(0gโ(๐ Mat (Poly1โ๐
)))) = 0 ) |
71 | 57, 70 | sylan9eqr 2795 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))) = (0gโ(๐ Mat
(Poly1โ๐
)))) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) = 0 ) |
72 | 56, 71 | mpdan 686 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) = 0 ) |
73 | 72 | adantr 482 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) โ ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) = 0 ) |
74 | 48, 73 | eqtrd 2773 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐)))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) |
75 | 74 | ex 414 |
. . 3
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 )) |
76 | 75 | rexlimdvva 3202 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = ((๐ โ (๐ ConstPolyMat ๐
) โฆ (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ ((coe1โ(๐ฅ๐๐ฆ))โ0)))โ((๐ Mat (Poly1โ๐
)) ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ(๐ Mat
(Poly1โ๐
))))((๐ matToPolyMat ๐
)โ๐))(.rโ(๐ Mat (Poly1โ๐
)))((๐ โ โ0 โฆ if(๐ = 0,
((0gโ(๐
Mat (Poly1โ๐
)))(-gโ(๐ Mat (Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ0)))), if(๐ = (๐ + 1), ((๐ matToPolyMat ๐
)โ(๐โ๐ )), if((๐ + 1) < ๐, (0gโ(๐ Mat (Poly1โ๐
))), (((๐ matToPolyMat ๐
)โ(๐โ(๐ โ 1)))(-gโ(๐ Mat
(Poly1โ๐
)))(((๐ matToPolyMat ๐
)โ๐)(.rโ(๐ Mat (Poly1โ๐
)))((๐ matToPolyMat ๐
)โ(๐โ๐))))))))โ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 )) |
77 | 39, 76 | mpd 15 |
1
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) |