Step | Hyp | Ref
| Expression |
1 | | chcoeffeq.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
2 | | chcoeffeq.b |
. . 3
โข ๐ต = (Baseโ๐ด) |
3 | | chcoeffeq.p |
. . 3
โข ๐ = (Poly1โ๐
) |
4 | | chcoeffeq.y |
. . 3
โข ๐ = (๐ Mat ๐) |
5 | | chcoeffeq.r |
. . 3
โข ร =
(.rโ๐) |
6 | | chcoeffeq.s |
. . 3
โข โ =
(-gโ๐) |
7 | | chcoeffeq.0 |
. . 3
โข 0 =
(0gโ๐) |
8 | | chcoeffeq.t |
. . 3
โข ๐ = (๐ matToPolyMat ๐
) |
9 | | chcoeffeq.c |
. . 3
โข ๐ถ = (๐ CharPlyMat ๐
) |
10 | | chcoeffeq.k |
. . 3
โข ๐พ = (๐ถโ๐) |
11 | | chcoeffeq.g |
. . 3
โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) |
12 | | chcoeffeq.w |
. . 3
โข ๐ = (Baseโ๐) |
13 | | chcoeffeq.1 |
. . 3
โข 1 =
(1rโ๐ด) |
14 | | chcoeffeq.m |
. . 3
โข โ = (
ยท๐ โ๐ด) |
15 | | chcoeffeq.u |
. . 3
โข ๐ = (๐ cPolyMatToMat ๐
) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | chcoeffeq 22258 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) |
17 | | 2fveq3 6851 |
. . . . . . 7
โข (๐ = ๐ โ (๐โ(๐บโ๐)) = (๐โ(๐บโ๐))) |
18 | | fveq2 6846 |
. . . . . . . 8
โข (๐ = ๐ โ ((coe1โ๐พ)โ๐) = ((coe1โ๐พ)โ๐)) |
19 | 18 | oveq1d 7376 |
. . . . . . 7
โข (๐ = ๐ โ (((coe1โ๐พ)โ๐) โ 1 ) =
(((coe1โ๐พ)โ๐) โ 1 )) |
20 | 17, 19 | eqeq12d 2749 |
. . . . . 6
โข (๐ = ๐ โ ((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ))) |
21 | 20 | cbvralvw 3224 |
. . . . 5
โข
(โ๐ โ
โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ โ๐ โ โ0
(๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) |
22 | | 2fveq3 6851 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐โ(๐บโ๐)) = (๐โ(๐บโ๐))) |
23 | | fveq2 6846 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((coe1โ๐พ)โ๐) = ((coe1โ๐พ)โ๐)) |
24 | 23 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (((coe1โ๐พ)โ๐) โ 1 ) =
(((coe1โ๐พ)โ๐) โ 1 )) |
25 | 22, 24 | eqeq12d 2749 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ))) |
26 | 25 | rspccva 3582 |
. . . . . . . . . . 11
โข
((โ๐ โ
โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง ๐ โ โ0) โ (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) |
27 | | simprll 778 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต)) |
28 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(Baseโ๐) =
(Baseโ๐) |
29 | 9, 1, 2, 3, 28 | chpmatply1 22204 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ถโ๐) โ (Baseโ๐)) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ถโ๐) โ (Baseโ๐)) |
31 | 10, 30 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ ๐พ โ (Baseโ๐)) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข
(coe1โ๐พ) = (coe1โ๐พ) |
33 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข
(Baseโ๐
) =
(Baseโ๐
) |
34 | 32, 28, 3, 33 | coe1f 21605 |
. . . . . . . . . . . . . . . . . . 19
โข (๐พ โ (Baseโ๐) โ
(coe1โ๐พ):โ0โถ(Baseโ๐
)) |
35 | 31, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ (coe1โ๐พ):โ0โถ(Baseโ๐
)) |
36 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . 20
โข
(Baseโ๐
)
โ V |
37 | | nn0ex 12427 |
. . . . . . . . . . . . . . . . . . . 20
โข
โ0 โ V |
38 | 36, 37 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . 19
โข
((Baseโ๐
)
โ V โง โ0 โ V) |
39 | | elmapg 8784 |
. . . . . . . . . . . . . . . . . . 19
โข
(((Baseโ๐
)
โ V โง โ0 โ V) โ
((coe1โ๐พ)
โ ((Baseโ๐
)
โm โ0) โ (coe1โ๐พ):โ0โถ(Baseโ๐
))) |
40 | 38, 39 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ ((coe1โ๐พ) โ ((Baseโ๐
) โm
โ0) โ (coe1โ๐พ):โ0โถ(Baseโ๐
))) |
41 | 35, 40 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ (coe1โ๐พ) โ ((Baseโ๐
) โm
โ0)) |
42 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ ๐ โ โ0) |
43 | | cayhamlem.e1 |
. . . . . . . . . . . . . . . . . 18
โข โ =
(.gโ(mulGrpโ๐ด)) |
44 | | cayhamlem.r |
. . . . . . . . . . . . . . . . . 18
โข ยท =
(.rโ๐ด) |
45 | 33, 1, 2, 13, 14, 43, 44 | cayhamlem2 22256 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ((coe1โ๐พ) โ ((Baseโ๐
) โm
โ0) โง ๐ โ โ0)) โ
(((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท
(((coe1โ๐พ)โ๐) โ 1 ))) |
46 | 27, 41, 42, 45 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ )))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท
(((coe1โ๐พ)โ๐) โ 1 ))) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . 15
โข (((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง (๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท
(((coe1โ๐พ)โ๐) โ 1 ))) |
48 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
โข ((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ ((๐ โ ๐) ยท (๐โ(๐บโ๐))) = ((๐ โ ๐) ยท
(((coe1โ๐พ)โ๐) โ 1 ))) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง (๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))))) โ ((๐ โ ๐) ยท (๐โ(๐บโ๐))) = ((๐ โ ๐) ยท
(((coe1โ๐พ)โ๐) โ 1 ))) |
50 | 47, 49 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
โข (((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง (๐ โ โ0
โง (((๐ โ Fin โง
๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐)))) |
51 | 50 | exp32 422 |
. . . . . . . . . . . . 13
โข ((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ (๐ โ โ0
โ ((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐)))))) |
52 | 51 | com12 32 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐)))))) |
53 | 52 | adantl 483 |
. . . . . . . . . . 11
โข
((โ๐ โ
โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง ๐ โ โ0) โ ((๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐)))))) |
54 | 26, 53 | mpd 15 |
. . . . . . . . . 10
โข
((โ๐ โ
โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง ๐ โ โ0) โ ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐))))) |
55 | 54 | com12 32 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ ((โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โง ๐ โ โ0) โ
(((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐))))) |
56 | 55 | impl 457 |
. . . . . . . 8
โข
((((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) โง ๐ โ โ0)
โ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)) = ((๐ โ ๐) ยท (๐โ(๐บโ๐)))) |
57 | 56 | mpteq2dva 5209 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) โ (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐))) = (๐ โ โ0 โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐))))) |
58 | 57 | oveq2d 7377 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 )) โ (๐ด ฮฃg
(๐ โ
โ0 โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐)))))) |
59 | 58 | ex 414 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ (๐ด ฮฃg
(๐ โ
โ0 โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐))))))) |
60 | 21, 59 | biimtrid 241 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ (๐ด ฮฃg
(๐ โ
โ0 โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐))))))) |
61 | 60 | reximdva 3162 |
. . 3
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โ (โ๐ โ (๐ต โm (0...๐ ))โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐))))))) |
62 | 61 | reximdva 3162 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))โ๐ โ โ0 (๐โ(๐บโ๐)) = (((coe1โ๐พ)โ๐) โ 1 ) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐))))))) |
63 | 16, 62 | mpd 15 |
1
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ด ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐) โ (๐ โ ๐)))) = (๐ด ฮฃg (๐ โ โ0
โฆ ((๐ โ ๐) ยท (๐โ(๐บโ๐)))))) |