Step | Hyp | Ref
| Expression |
1 | | chpdmat.p |
. . . . . 6
β’ π = (Poly1βπ
) |
2 | 1 | ply1ring 21642 |
. . . . 5
β’ (π
β Ring β π β Ring) |
3 | 2 | 3ad2ant2 1135 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β Ring) |
4 | 3 | adantr 482 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β π β Ring) |
5 | | chpdmat.c |
. . . . . . 7
β’ πΆ = (π CharPlyMat π
) |
6 | | chpdmat.a |
. . . . . . 7
β’ π΄ = (π Mat π
) |
7 | | chpdmat.s |
. . . . . . 7
β’ π = (algScβπ) |
8 | | chpdmat.b |
. . . . . . 7
β’ π΅ = (Baseβπ΄) |
9 | | chpdmat.x |
. . . . . . 7
β’ π = (var1βπ
) |
10 | | chpdmat.0 |
. . . . . . 7
β’ 0 =
(0gβπ
) |
11 | | chpdmat.g |
. . . . . . 7
β’ πΊ = (mulGrpβπ) |
12 | | chpdmat.m |
. . . . . . 7
β’ β =
(-gβπ) |
13 | | chpdmatlem.q |
. . . . . . 7
β’ π = (π Mat π) |
14 | | chpdmatlem.1 |
. . . . . . 7
β’ 1 =
(1rβπ) |
15 | | chpdmatlem.m |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
16 | 5, 1, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | chpdmatlem0 22209 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β (π Β· 1 ) β (Baseβπ)) |
17 | 16 | 3adant3 1133 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π Β· 1 ) β (Baseβπ)) |
18 | | chpdmatlem.t |
. . . . . 6
β’ π = (π matToPolyMat π
) |
19 | 18, 6, 8, 1, 13 | mat2pmatbas 22098 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β (Baseβπ)) |
20 | 17, 19 | jca 513 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β ((π Β· 1 ) β (Baseβπ) β§ (πβπ) β (Baseβπ))) |
21 | 20 | adantr 482 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β ((π Β· 1 ) β (Baseβπ) β§ (πβπ) β (Baseβπ))) |
22 | | simpr 486 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β πΎ β π) |
23 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
24 | | chpdmatlem.z |
. . . 4
β’ π = (-gβπ) |
25 | 13, 23, 24, 12 | matsubgcell 21806 |
. . 3
β’ ((π β Ring β§ ((π Β· 1 ) β (Baseβπ) β§ (πβπ) β (Baseβπ)) β§ (πΎ β π β§ πΎ β π)) β (πΎ((π Β· 1 )π(πβπ))πΎ) = ((πΎ(π Β· 1 )πΎ) β (πΎ(πβπ)πΎ))) |
26 | 4, 21, 22, 22, 25 | syl112anc 1375 |
. 2
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ((π Β· 1 )π(πβπ))πΎ) = ((πΎ(π Β· 1 )πΎ) β (πΎ(πβπ)πΎ))) |
27 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
28 | 9, 1, 27 | vr1cl 21611 |
. . . . . . . . 9
β’ (π
β Ring β π β (Baseβπ)) |
29 | 28 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β π β (Baseβπ)) |
30 | 1, 13 | pmatring 22064 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β π β Ring) |
31 | 23, 14 | ringidcl 19997 |
. . . . . . . . 9
β’ (π β Ring β 1 β
(Baseβπ)) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β 1 β
(Baseβπ)) |
33 | 29, 32 | jca 513 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β (π β (Baseβπ) β§ 1 β (Baseβπ))) |
34 | 33 | 3adant3 1133 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β (Baseβπ) β§ 1 β (Baseβπ))) |
35 | 34 | adantr 482 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (π β (Baseβπ) β§ 1 β (Baseβπ))) |
36 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
37 | 13, 23, 27, 15, 36 | matvscacell 21808 |
. . . . 5
β’ ((π β Ring β§ (π β (Baseβπ) β§ 1 β (Baseβπ)) β§ (πΎ β π β§ πΎ β π)) β (πΎ(π Β· 1 )πΎ) = (π(.rβπ)(πΎ 1 πΎ))) |
38 | 4, 35, 22, 22, 37 | syl112anc 1375 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ(π Β· 1 )πΎ) = (π(.rβπ)(πΎ 1 πΎ))) |
39 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
40 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
41 | | simpl1 1192 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β π β Fin) |
42 | 13, 39, 40, 41, 4, 22, 22, 14 | mat1ov 21820 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ 1 πΎ) = if(πΎ = πΎ, (1rβπ), (0gβπ))) |
43 | | eqid 2733 |
. . . . . . 7
β’ πΎ = πΎ |
44 | 43 | iftruei 4497 |
. . . . . 6
β’ if(πΎ = πΎ, (1rβπ), (0gβπ)) = (1rβπ) |
45 | 42, 44 | eqtrdi 2789 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ 1 πΎ) = (1rβπ)) |
46 | 45 | oveq2d 7377 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (π(.rβπ)(πΎ 1 πΎ)) = (π(.rβπ)(1rβπ))) |
47 | 2, 28 | jca 513 |
. . . . . . 7
β’ (π
β Ring β (π β Ring β§ π β (Baseβπ))) |
48 | 47 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β Ring β§ π β (Baseβπ))) |
49 | 27, 36, 39 | ringridm 20001 |
. . . . . 6
β’ ((π β Ring β§ π β (Baseβπ)) β (π(.rβπ)(1rβπ)) = π) |
50 | 48, 49 | syl 17 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π(.rβπ)(1rβπ)) = π) |
51 | 50 | adantr 482 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (π(.rβπ)(1rβπ)) = π) |
52 | 38, 46, 51 | 3eqtrd 2777 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ(π Β· 1 )πΎ) = π) |
53 | 18, 6, 8, 1, 7 | mat2pmatvalel 22097 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (πΎ β π β§ πΎ β π)) β (πΎ(πβπ)πΎ) = (πβ(πΎππΎ))) |
54 | 53 | anabsan2 673 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ(πβπ)πΎ) = (πβ(πΎππΎ))) |
55 | 52, 54 | oveq12d 7379 |
. 2
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β ((πΎ(π Β· 1 )πΎ) β (πΎ(πβπ)πΎ)) = (π β (πβ(πΎππΎ)))) |
56 | 26, 55 | eqtrd 2773 |
1
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ πΎ β π) β (πΎ((π Β· 1 )π(πβπ))πΎ) = (π β (πβ(πΎππΎ)))) |