Step | Hyp | Ref
| Expression |
1 | | cayleyhamilton0.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
2 | | cayleyhamilton0.b |
. . 3
โข ๐ต = (Baseโ๐ด) |
3 | | cayleyhamilton0.p |
. . 3
โข ๐ = (Poly1โ๐
) |
4 | | cayleyhamilton0.y |
. . 3
โข ๐ = (๐ Mat ๐) |
5 | | cayleyhamilton0.r |
. . 3
โข ร =
(.rโ๐) |
6 | | cayleyhamilton0.s |
. . 3
โข โ =
(-gโ๐) |
7 | | cayleyhamilton0.z |
. . 3
โข ๐ = (0gโ๐) |
8 | | cayleyhamilton0.t |
. . 3
โข ๐ = (๐ matToPolyMat ๐
) |
9 | | cayleyhamilton0.c |
. . 3
โข ๐ถ = (๐ CharPlyMat ๐
) |
10 | | eqid 2733 |
. . 3
โข (๐ถโ๐) = (๐ถโ๐) |
11 | | cayleyhamilton0.g |
. . 3
โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, (๐ โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, ๐, ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) |
12 | | cayleyhamilton0.w |
. . 3
โข ๐ = (Baseโ๐) |
13 | | cayleyhamilton0.1 |
. . 3
โข 1 =
(1rโ๐ด) |
14 | | cayleyhamilton0.m |
. . 3
โข โ = (
ยท๐ โ๐ด) |
15 | | cayleyhamilton0.u |
. . 3
โข ๐ = (๐ cPolyMatToMat ๐
) |
16 | | cayleyhamilton0.e1 |
. . 3
โข โ =
(.gโ(mulGrpโ๐ด)) |
17 | | cayleyhamilton0.e2 |
. . 3
โข ๐ธ =
(.gโ(mulGrpโ๐)) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17 | cayhamlem4 22260 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))))) |
19 | | cayleyhamilton0.k |
. . . . . . . . . . . . 13
โข ๐พ = (coe1โ(๐ถโ๐)) |
20 | 19 | eqcomi 2742 |
. . . . . . . . . . . 12
โข
(coe1โ(๐ถโ๐)) = ๐พ |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ
(coe1โ(๐ถโ๐)) = ๐พ) |
22 | 21 | fveq1d 6848 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ
((coe1โ(๐ถโ๐))โ๐) = (๐พโ๐)) |
23 | 22 | oveq1d 7376 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ
(((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)) = ((๐พโ๐) โ (๐ โ ๐))) |
24 | 23 | mpteq2dva 5209 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ โ โ0 โฆ
(((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐))) = (๐ โ โ0 โฆ ((๐พโ๐) โ (๐ โ ๐)))) |
25 | 24 | oveq2d 7377 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐))))) |
26 | 25 | eqeq1d 2735 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))))) |
27 | 26 | biimpa 478 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))))) |
28 | | oveq1 7368 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐๐ธ(๐โ๐)) = (๐๐ธ(๐โ๐))) |
29 | | fveq2 6846 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐บโ๐) = (๐บโ๐)) |
30 | 28, 29 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)) = ((๐๐ธ(๐โ๐)) ร (๐บโ๐))) |
31 | 30 | cbvmptv 5222 |
. . . . . . . . 9
โข (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))) = (๐ โ โ0 โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))) |
32 | 31 | oveq2i 7372 |
. . . . . . . 8
โข (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))) |
33 | 1, 2, 3, 4, 5, 6, 7, 8, 11, 17 | cayhamlem1 22238 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))) = ๐) |
34 | 32, 33 | eqtrid 2785 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))) = ๐) |
35 | | fveq2 6846 |
. . . . . . . 8
โข ((๐ ฮฃg
(๐ โ
โ0 โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))) = ๐ โ (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) = (๐โ๐)) |
36 | | crngring 19984 |
. . . . . . . . . . . . 13
โข (๐
โ CRing โ ๐
โ Ring) |
37 | 36 | anim2i 618 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ CRing) โ (๐ โ Fin โง ๐
โ Ring)) |
38 | 37 | 3adant3 1133 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐
โ Ring)) |
39 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(0gโ๐ด) = (0gโ๐ด) |
40 | 1, 15, 3, 4, 39, 7 | m2cpminv0 22133 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐โ๐) = (0gโ๐ด)) |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐โ๐) = (0gโ๐ด)) |
42 | | cayleyhamilton0.0 |
. . . . . . . . . 10
โข 0 =
(0gโ๐ด) |
43 | 41, 42 | eqtr4di 2791 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐โ๐) = 0 ) |
44 | 43 | adantr 482 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐โ๐) = 0 ) |
45 | 35, 44 | sylan9eqr 2795 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))) = ๐) โ (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) = 0 ) |
46 | 34, 45 | mpdan 686 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) = 0 ) |
47 | 46 | adantr 482 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))))) โ (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) = 0 ) |
48 | 27, 47 | eqtrd 2773 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง (๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐)))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) |
49 | 48 | ex 414 |
. . 3
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ((๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 )) |
50 | 49 | rexlimdvva 3202 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐ถโ๐))โ๐) โ (๐ โ ๐)))) = (๐โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐๐ธ(๐โ๐)) ร (๐บโ๐))))) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 )) |
51 | 18, 50 | mpd 15 |
1
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ด ฮฃg (๐ โ โ0
โฆ ((๐พโ๐) โ (๐ โ ๐)))) = 0 ) |