Step | Hyp | Ref
| Expression |
1 | | cayleyhamilton.a |
. . . 4
Mat |
2 | | cayleyhamilton.b |
. . . 4
|
3 | | eqid 2622 |
. . . 4
Poly1 Poly1 |
4 | | eqid 2622 |
. . . 4
Mat Poly1 Mat Poly1 |
5 | | eqid 2622 |
. . . 4
Mat Poly1
Mat Poly1 |
6 | | eqid 2622 |
. . . 4
Mat Poly1 Mat Poly1 |
7 | | eqid 2622 |
. . . 4
Mat Poly1
Mat Poly1 |
8 | | eqid 2622 |
. . . 4
matToPolyMat matToPolyMat |
9 | | cayleyhamilton.c |
. . . 4
CharPlyMat
|
10 | | eqid 2622 |
. . . 4
|
11 | | eqeq1 2626 |
. . . . . 6
|
12 | | eqeq1 2626 |
. . . . . . 7
|
13 | | breq2 4657 |
. . . . . . . 8
|
14 | | oveq1 6657 |
. . . . . . . . . . 11
|
15 | 14 | fveq2d 6195 |
. . . . . . . . . 10
|
16 | 15 | fveq2d 6195 |
. . . . . . . . 9
matToPolyMat
matToPolyMat |
17 | | fveq2 6191 |
. . . . . . . . . . 11
|
18 | 17 | fveq2d 6195 |
. . . . . . . . . 10
matToPolyMat
matToPolyMat |
19 | 18 | oveq2d 6666 |
. . . . . . . . 9
matToPolyMat Mat Poly1 matToPolyMat
matToPolyMat Mat Poly1 matToPolyMat |
20 | 16, 19 | oveq12d 6668 |
. . . . . . . 8
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat |
21 | 13, 20 | ifbieq2d 4111 |
. . . . . . 7
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat |
22 | 12, 21 | ifbieq2d 4111 |
. . . . . 6
matToPolyMat Mat Poly1
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
23 | 11, 22 | ifbieq2d 4111 |
. . . . 5
Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
24 | 23 | cbvmptv 4750 |
. . . 4
Mat Poly1 Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat matToPolyMat Mat Poly1
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
matToPolyMat Mat Poly1
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat |
25 | | eqid 2622 |
. . . 4
Mat Poly1 Mat Poly1 |
26 | | eqid 2622 |
. . . 4
|
27 | | cayleyhamilton.m |
. . . 4
|
28 | | eqid 2622 |
. . . 4
cPolyMatToMat cPolyMatToMat |
29 | | cayleyhamilton.e |
. . . 4
.gmulGrp |
30 | | eqid 2622 |
. . . 4
.gmulGrp Mat Poly1 .gmulGrp Mat Poly1 |
31 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
24, 25, 26, 27, 28, 29, 30 | cayhamlem4 20693 |
. . 3
g coe1 cPolyMatToMat Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
32 | | eqid 2622 |
. . . . . . . . 9
ConstPolyMat ConstPolyMat |
33 | 28, 32 | cpm2mfval 20554 |
. . . . . . . 8
cPolyMatToMat ConstPolyMat coe1 |
34 | 33 | eqcomd 2628 |
. . . . . . 7
ConstPolyMat coe1
cPolyMatToMat |
35 | 34 | 3adant3 1081 |
. . . . . 6
ConstPolyMat coe1 cPolyMatToMat |
36 | 35 | fveq1d 6193 |
. . . . 5
ConstPolyMat coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat cPolyMatToMat Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
37 | 36 | eqeq2d 2632 |
. . . 4
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
g coe1
cPolyMatToMat Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
38 | 37 | 2rexbidv 3057 |
. . 3
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
g coe1 cPolyMatToMat Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
39 | 31, 38 | mpbird 247 |
. 2
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
40 | | cayleyhamilton.k |
. . . . . . . . . . . . 13
coe1 |
41 | 40 | eqcomi 2631 |
. . . . . . . . . . . 12
coe1 |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
coe1 |
43 | 42 | fveq1d 6193 |
. . . . . . . . . 10
coe1 |
44 | 43 | oveq1d 6665 |
. . . . . . . . 9
coe1
|
45 | 44 | mpteq2dva 4744 |
. . . . . . . 8
coe1
|
46 | 45 | oveq2d 6666 |
. . . . . . 7
g
coe1
g
|
47 | 46 | eqeq1d 2624 |
. . . . . 6
g
coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
g ConstPolyMat coe1 Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
48 | 47 | biimpa 501 |
. . . . 5
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat g
ConstPolyMat coe1 Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
49 | | oveq1 6657 |
. . . . . . . . . . . 12
.gmulGrp Mat Poly1 matToPolyMat .gmulGrp Mat Poly1 matToPolyMat |
50 | | fveq2 6191 |
. . . . . . . . . . . 12
Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
51 | 49, 50 | oveq12d 6668 |
. . . . . . . . . . 11
.gmulGrp Mat Poly1 matToPolyMat Mat Poly1
Mat Poly1 Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat matToPolyMat Mat Poly1
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat .gmulGrp Mat Poly1 matToPolyMat Mat Poly1
Mat Poly1 Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat matToPolyMat Mat Poly1
matToPolyMat Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat |
52 | 51 | cbvmptv 4750 |
. . . . . . . . . 10
.gmulGrp Mat Poly1 matToPolyMat Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
.gmulGrp Mat Poly1 matToPolyMat Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
53 | 52 | oveq2i 6661 |
. . . . . . . . 9
Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
54 | 53 | a1i 11 |
. . . . . . . 8
Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
55 | 1, 2, 3, 4, 5, 6, 7, 8, 24, 30 | cayhamlem1 20671 |
. . . . . . . 8
Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 |
56 | 54, 55 | eqtrd 2656 |
. . . . . . 7
Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 |
57 | | fveq2 6191 |
. . . . . . . 8
Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1
ConstPolyMat coe1 Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
ConstPolyMat coe1
Mat Poly1 |
58 | | crngring 18558 |
. . . . . . . . . . . . 13
|
59 | 58 | anim2i 593 |
. . . . . . . . . . . 12
|
60 | 59 | 3adant3 1081 |
. . . . . . . . . . 11
|
61 | 28, 32 | cpm2mfval 20554 |
. . . . . . . . . . . . . 14
cPolyMatToMat ConstPolyMat coe1 |
62 | 61 | eqcomd 2628 |
. . . . . . . . . . . . 13
ConstPolyMat coe1
cPolyMatToMat |
63 | 62 | fveq1d 6193 |
. . . . . . . . . . . 12
ConstPolyMat coe1
Mat Poly1 cPolyMatToMat Mat Poly1 |
64 | | eqid 2622 |
. . . . . . . . . . . . 13
|
65 | 1, 28, 3, 4, 64, 7 | m2cpminv0 20566 |
. . . . . . . . . . . 12
cPolyMatToMat
Mat Poly1 |
66 | 63, 65 | eqtrd 2656 |
. . . . . . . . . . 11
ConstPolyMat coe1
Mat Poly1 |
67 | 60, 66 | syl 17 |
. . . . . . . . . 10
ConstPolyMat coe1 Mat Poly1 |
68 | | cayleyhamilton.0 |
. . . . . . . . . 10
|
69 | 67, 68 | syl6eqr 2674 |
. . . . . . . . 9
ConstPolyMat coe1 Mat Poly1 |
70 | 69 | adantr 481 |
. . . . . . . 8
ConstPolyMat
coe1
Mat Poly1 |
71 | 57, 70 | sylan9eqr 2678 |
. . . . . . 7
Mat Poly1 g .gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat Mat Poly1 ConstPolyMat coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
72 | 56, 71 | mpdan 702 |
. . . . . 6
ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
73 | 72 | adantr 481 |
. . . . 5
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat |
74 | 48, 73 | eqtrd 2656 |
. . . 4
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat g
|
75 | 74 | ex 450 |
. . 3
g
coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat g
|
76 | 75 | rexlimdvva 3038 |
. 2
g coe1 ConstPolyMat
coe1 Mat Poly1 g
.gmulGrp Mat Poly1 matToPolyMat
Mat Poly1 Mat Poly1 Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat
matToPolyMat
Mat Poly1 matToPolyMat Mat Poly1 matToPolyMat
Mat Poly1
matToPolyMat g
|
77 | 39, 76 | mpd 15 |
1
g
|