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 | ad4antr 731 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β π β Ring) |
5 | | chpdmat.c |
. . . . . 6
β’ πΆ = (π CharPlyMat π
) |
6 | | chpdmat.a |
. . . . . 6
β’ π΄ = (π Mat π
) |
7 | | chpdmat.s |
. . . . . 6
β’ π = (algScβπ) |
8 | | chpdmat.b |
. . . . . 6
β’ π΅ = (Baseβπ΄) |
9 | | chpdmat.x |
. . . . . 6
β’ π = (var1βπ
) |
10 | | chpdmat.0 |
. . . . . 6
β’ 0 =
(0gβπ
) |
11 | | chpdmat.g |
. . . . . 6
β’ πΊ = (mulGrpβπ) |
12 | | chpdmat.m |
. . . . . 6
β’ β =
(-gβπ) |
13 | | chpdmatlem.q |
. . . . . 6
β’ π = (π Mat π) |
14 | | chpdmatlem.1 |
. . . . . 6
β’ 1 =
(1rβπ) |
15 | | chpdmatlem.m |
. . . . . 6
β’ Β· = (
Β·π βπ) |
16 | 5, 1, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | chpdmatlem0 22209 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β (π Β· 1 ) β (Baseβπ)) |
17 | 16 | 3adant3 1133 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π Β· 1 ) β (Baseβπ)) |
18 | 17 | ad4antr 731 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π Β· 1 ) β (Baseβπ)) |
19 | | chpdmatlem.t |
. . . . 5
β’ π = (π matToPolyMat π
) |
20 | 19, 6, 8, 1, 13 | mat2pmatbas 22098 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β (Baseβπ)) |
21 | 20 | ad4antr 731 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (πβπ) β (Baseβπ)) |
22 | | simpr 486 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β π β π) |
23 | 22 | anim1i 616 |
. . . 4
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β (π β π β§ π β π)) |
24 | 23 | ad2antrr 725 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π β π β§ π β π)) |
25 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
26 | | chpdmatlem.z |
. . . 4
β’ π = (-gβπ) |
27 | 13, 25, 26, 12 | matsubgcell 21806 |
. . 3
β’ ((π β Ring β§ ((π Β· 1 ) β (Baseβπ) β§ (πβπ) β (Baseβπ)) β§ (π β π β§ π β π)) β (π((π Β· 1 )π(πβπ))π) = ((π(π Β· 1 )π) β (π(πβπ)π))) |
28 | 4, 18, 21, 24, 27 | syl121anc 1376 |
. 2
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π((π Β· 1 )π(πβπ))π) = ((π(π Β· 1 )π) β (π(πβπ)π))) |
29 | 3 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β π β Ring) |
30 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
31 | 9, 1, 30 | vr1cl 21611 |
. . . . . . . . 9
β’ (π
β Ring β π β (Baseβπ)) |
32 | 31 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β (Baseβπ)) |
33 | 1, 13 | pmatring 22064 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β π β Ring) |
34 | 33 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β Ring) |
35 | 25, 14 | ringidcl 19997 |
. . . . . . . . 9
β’ (π β Ring β 1 β
(Baseβπ)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β 1 β (Baseβπ)) |
37 | 32, 36 | jca 513 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β (Baseβπ) β§ 1 β (Baseβπ))) |
38 | 37 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β (π β (Baseβπ) β§ 1 β (Baseβπ))) |
39 | 29, 38, 23 | 3jca 1129 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β (π β Ring β§ (π β (Baseβπ) β§ 1 β (Baseβπ)) β§ (π β π β§ π β π))) |
40 | 39 | ad2antrr 725 |
. . . 4
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π β Ring β§ (π β (Baseβπ) β§ 1 β (Baseβπ)) β§ (π β π β§ π β π))) |
41 | | eqid 2733 |
. . . . 5
β’
(.rβπ) = (.rβπ) |
42 | 13, 25, 30, 15, 41 | matvscacell 21808 |
. . . 4
β’ ((π β Ring β§ (π β (Baseβπ) β§ 1 β (Baseβπ)) β§ (π β π β§ π β π)) β (π(π Β· 1 )π) = (π(.rβπ)(π 1 π))) |
43 | 40, 42 | syl 17 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π(π Β· 1 )π) = (π(.rβπ)(π 1 π))) |
44 | 43 | oveq1d 7376 |
. 2
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β ((π(π Β· 1 )π) β (π(πβπ)π)) = ((π(.rβπ)(π 1 π)) β (π(πβπ)π))) |
45 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ) = (1rβπ) |
46 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
47 | | simpll1 1213 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β π β Fin) |
48 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β π β π) |
49 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β π β π) |
50 | 13, 45, 46, 47, 29, 48, 49, 14 | mat1ov 21820 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β (π 1 π) = if(π = π, (1rβπ), (0gβπ))) |
51 | | ifnefalse 4502 |
. . . . . . . 8
β’ (π β π β if(π = π, (1rβπ), (0gβπ)) = (0gβπ)) |
52 | 50, 51 | sylan9eq 2793 |
. . . . . . 7
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β (π 1 π) = (0gβπ)) |
53 | 52 | oveq2d 7377 |
. . . . . 6
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β (π(.rβπ)(π 1 π)) = (π(.rβπ)(0gβπ))) |
54 | 2, 31 | jca 513 |
. . . . . . . . . 10
β’ (π
β Ring β (π β Ring β§ π β (Baseβπ))) |
55 | 54 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β Ring β§ π β (Baseβπ))) |
56 | 30, 41, 46 | ringrz 20020 |
. . . . . . . . 9
β’ ((π β Ring β§ π β (Baseβπ)) β (π(.rβπ)(0gβπ)) = (0gβπ)) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π(.rβπ)(0gβπ)) = (0gβπ)) |
58 | 57 | adantr 482 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β (π(.rβπ)(0gβπ)) = (0gβπ)) |
59 | 58 | ad2antrr 725 |
. . . . . 6
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β (π(.rβπ)(0gβπ)) = (0gβπ)) |
60 | 53, 59 | eqtrd 2773 |
. . . . 5
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β (π(.rβπ)(π 1 π)) = (0gβπ)) |
61 | 60 | adantr 482 |
. . . 4
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π(.rβπ)(π 1 π)) = (0gβπ)) |
62 | | simpll 766 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β (π β Fin β§ π
β Ring β§ π β π΅)) |
63 | 62, 23 | jca 513 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ π β π) β§ π β π) β ((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π))) |
64 | 63 | ad2antrr 725 |
. . . . 5
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β ((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π))) |
65 | 19, 6, 8, 1, 7 | mat2pmatvalel 22097 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β (π(πβπ)π) = (πβ(πππ))) |
66 | 64, 65 | syl 17 |
. . . 4
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π(πβπ)π) = (πβ(πππ))) |
67 | 61, 66 | oveq12d 7379 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β ((π(.rβπ)(π 1 π)) β (π(πβπ)π)) = ((0gβπ) β (πβ(πππ)))) |
68 | | fveq2 6846 |
. . . . . 6
β’ ((πππ) = 0 β (πβ(πππ)) = (πβ 0 )) |
69 | 68 | adantl 483 |
. . . . 5
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (πβ(πππ)) = (πβ 0 )) |
70 | 1, 7, 10, 46 | ply1scl0 21684 |
. . . . . . 7
β’ (π
β Ring β (πβ 0 ) =
(0gβπ)) |
71 | 70 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβ 0 ) =
(0gβπ)) |
72 | 71 | ad4antr 731 |
. . . . 5
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (πβ 0 ) =
(0gβπ)) |
73 | 69, 72 | eqtrd 2773 |
. . . 4
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (πβ(πππ)) = (0gβπ)) |
74 | 73 | oveq2d 7377 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β
((0gβπ)
β
(πβ(πππ))) = ((0gβπ) β
(0gβπ))) |
75 | | ringgrp 19977 |
. . . . . . . 8
β’ (π β Ring β π β Grp) |
76 | 2, 75 | syl 17 |
. . . . . . 7
β’ (π
β Ring β π β Grp) |
77 | 30, 46 | grpidcl 18786 |
. . . . . . 7
β’ (π β Grp β
(0gβπ)
β (Baseβπ)) |
78 | 76, 77 | jccir 523 |
. . . . . 6
β’ (π
β Ring β (π β Grp β§
(0gβπ)
β (Baseβπ))) |
79 | 78 | 3ad2ant2 1135 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β Grp β§ (0gβπ) β (Baseβπ))) |
80 | 30, 46, 12 | grpsubid 18839 |
. . . . 5
β’ ((π β Grp β§
(0gβπ)
β (Baseβπ))
β ((0gβπ) β
(0gβπ)) =
(0gβπ)) |
81 | 79, 80 | syl 17 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β ((0gβπ) β
(0gβπ)) =
(0gβπ)) |
82 | 81 | ad4antr 731 |
. . 3
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β
((0gβπ)
β
(0gβπ)) =
(0gβπ)) |
83 | 67, 74, 82 | 3eqtrd 2777 |
. 2
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β ((π(.rβπ)(π 1 π)) β (π(πβπ)π)) = (0gβπ)) |
84 | 28, 44, 83 | 3eqtrd 2777 |
1
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ π β π) β§ π β π) β§ π β π) β§ (πππ) = 0 ) β (π((π Β· 1 )π(πβπ))π) = (0gβπ)) |