Step | Hyp | Ref
| Expression |
1 | | chp0mat.c |
. . 3
β’ πΆ = (π CharPlyMat π
) |
2 | | chp0mat.p |
. . 3
β’ π = (Poly1βπ
) |
3 | | chp0mat.a |
. . 3
β’ π΄ = (π Mat π
) |
4 | | chp0mat.x |
. . 3
β’ π = (var1βπ
) |
5 | | chp0mat.g |
. . 3
β’ πΊ = (mulGrpβπ) |
6 | | chp0mat.m |
. . 3
β’ β =
(.gβπΊ) |
7 | | chpscmat.d |
. . 3
β’ π· = {π β (Baseβπ΄) β£ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))} |
8 | | chpscmat.s |
. . 3
β’ π = (algScβπ) |
9 | | chpscmat.m |
. . 3
β’ β =
(-gβπ) |
10 | | chpscmatgsum.f |
. . 3
β’ πΉ = (.gβπ) |
11 | | chpscmatgsum.h |
. . 3
β’ π» = (mulGrpβπ
) |
12 | | chpscmatgsum.e |
. . 3
β’ πΈ = (.gβπ») |
13 | | chpscmatgsum.i |
. . 3
β’ πΌ = (invgβπ
) |
14 | | chpscmatgsum.s |
. . 3
β’ Β· = (
Β·π βπ) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | chpscmatgsumbin 22216 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (πΆβπ) = (π Ξ£g (π β
(0...(β―βπ))
β¦ (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π)))))) |
16 | | crngring 19984 |
. . . . . . . . 9
β’ (π
β CRing β π
β Ring) |
17 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β π
β Ring) |
18 | 2 | ply1lmod 21646 |
. . . . . . . 8
β’ (π
β Ring β π β LMod) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing) β π β LMod) |
20 | 19 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β π β LMod) |
21 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
22 | 11, 21 | mgpbas 19910 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ») |
23 | 11 | ringmgp 19978 |
. . . . . . . . . 10
β’ (π
β Ring β π» β Mnd) |
24 | 17, 23 | syl 17 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing) β π» β Mnd) |
25 | 24 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β π» β Mnd) |
26 | | fznn0sub 13482 |
. . . . . . . . 9
β’ (π β
(0...(β―βπ))
β ((β―βπ)
β π) β
β0) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β ((β―βπ) β π) β
β0) |
28 | | ringgrp 19977 |
. . . . . . . . . . . 12
β’ (π
β Ring β π
β Grp) |
29 | 16, 28 | syl 17 |
. . . . . . . . . . 11
β’ (π
β CRing β π
β Grp) |
30 | 29 | adantl 483 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing) β π
β Grp) |
31 | | simp2 1138 |
. . . . . . . . . . . . 13
β’ ((π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½)) β π½ β π) |
32 | | elrabi 3643 |
. . . . . . . . . . . . . . 15
β’ (π β {π β (Baseβπ΄) β£ βπ β (Baseβπ
)βπ β π βπ β π (πππ) = if(π = π, π, (0gβπ
))} β π β (Baseβπ΄)) |
33 | 32, 7 | eleq2s 2852 |
. . . . . . . . . . . . . 14
β’ (π β π· β π β (Baseβπ΄)) |
34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½)) β π β (Baseβπ΄)) |
35 | 31, 31, 34 | 3jca 1129 |
. . . . . . . . . . . 12
β’ ((π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½)) β (π½ β π β§ π½ β π β§ π β (Baseβπ΄))) |
36 | 35 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (π½ β π β§ π½ β π β§ π β (Baseβπ΄))) |
37 | 3, 21 | matecl 21797 |
. . . . . . . . . . 11
β’ ((π½ β π β§ π½ β π β§ π β (Baseβπ΄)) β (π½ππ½) β (Baseβπ
)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (π½ππ½) β (Baseβπ
)) |
39 | 21, 13 | grpinvcl 18806 |
. . . . . . . . . 10
β’ ((π
β Grp β§ (π½ππ½) β (Baseβπ
)) β (πΌβ(π½ππ½)) β (Baseβπ
)) |
40 | 30, 38, 39 | syl2an2r 684 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (πΌβ(π½ππ½)) β (Baseβπ
)) |
41 | 40 | adantr 482 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (πΌβ(π½ππ½)) β (Baseβπ
)) |
42 | 22, 12, 25, 27, 41 | mulgnn0cld 18905 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (((β―βπ) β π)πΈ(πΌβ(π½ππ½))) β (Baseβπ
)) |
43 | 2 | ply1sca 21647 |
. . . . . . . . . . 11
β’ (π
β CRing β π
= (Scalarβπ)) |
44 | 43 | adantl 483 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing) β π
= (Scalarβπ)) |
45 | 44 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing) β
(Scalarβπ) = π
) |
46 | 45 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β
(Baseβ(Scalarβπ)) = (Baseβπ
)) |
47 | 46 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (Baseβ(Scalarβπ)) = (Baseβπ
)) |
48 | 42, 47 | eleqtrrd 2837 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (((β―βπ) β π)πΈ(πΌβ(π½ππ½))) β (Baseβ(Scalarβπ))) |
49 | | hashcl 14265 |
. . . . . . . 8
β’ (π β Fin β
(β―βπ) β
β0) |
50 | 49 | ad2antrr 725 |
. . . . . . 7
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (β―βπ) β
β0) |
51 | | elfzelz 13450 |
. . . . . . 7
β’ (π β
(0...(β―βπ))
β π β
β€) |
52 | | bccl 14231 |
. . . . . . 7
β’
(((β―βπ)
β β0 β§ π β β€) β ((β―βπ)Cπ) β
β0) |
53 | 50, 51, 52 | syl2an 597 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β ((β―βπ)Cπ) β
β0) |
54 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
55 | 5, 54 | mgpbas 19910 |
. . . . . . 7
β’
(Baseβπ) =
(BaseβπΊ) |
56 | 2 | ply1ring 21642 |
. . . . . . . . . 10
β’ (π
β Ring β π β Ring) |
57 | 5 | ringmgp 19978 |
. . . . . . . . . 10
β’ (π β Ring β πΊ β Mnd) |
58 | 16, 56, 57 | 3syl 18 |
. . . . . . . . 9
β’ (π
β CRing β πΊ β Mnd) |
59 | 58 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β πΊ β Mnd) |
60 | 59 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β πΊ β Mnd) |
61 | | elfznn0 13543 |
. . . . . . . 8
β’ (π β
(0...(β―βπ))
β π β
β0) |
62 | 61 | adantl 483 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β π β β0) |
63 | 4, 2, 54 | vr1cl 21611 |
. . . . . . . . 9
β’ (π
β Ring β π β (Baseβπ)) |
64 | 17, 63 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β π β (Baseβπ)) |
65 | 64 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β π β (Baseβπ)) |
66 | 55, 6, 60, 62, 65 | mulgnn0cld 18905 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (π β π) β (Baseβπ)) |
67 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
68 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
69 | | eqid 2733 |
. . . . . . 7
β’
(.gβ(Scalarβπ)) =
(.gβ(Scalarβπ)) |
70 | 54, 67, 14, 68, 10, 69 | lmodvsmmulgdi 20401 |
. . . . . 6
β’ ((π β LMod β§
((((β―βπ)
β π)πΈ(πΌβ(π½ππ½))) β (Baseβ(Scalarβπ)) β§ ((β―βπ)Cπ) β β0 β§ (π β π) β (Baseβπ))) β (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π))) = ((((β―βπ)Cπ)(.gβ(Scalarβπ))(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))) |
71 | 20, 48, 53, 66, 70 | syl13anc 1373 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π))) = ((((β―βπ)Cπ)(.gβ(Scalarβπ))(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))) |
72 | | chpscmatgsum.z |
. . . . . . . . 9
β’ π = (.gβπ
) |
73 | 44 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing) β
(.gβπ
) =
(.gβ(Scalarβπ))) |
74 | 72, 73 | eqtr2id 2786 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β
(.gβ(Scalarβπ)) = π) |
75 | 74 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β
(.gβ(Scalarβπ)) = π) |
76 | 75 | oveqd 7378 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (((β―βπ)Cπ)(.gβ(Scalarβπ))(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) = (((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½))))) |
77 | 76 | oveq1d 7376 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β ((((β―βπ)Cπ)(.gβ(Scalarβπ))(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π)) = ((((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))) |
78 | 71, 77 | eqtrd 2773 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β§ π β (0...(β―βπ))) β (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π))) = ((((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))) |
79 | 78 | mpteq2dva 5209 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (π β (0...(β―βπ)) β¦ (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π)))) = (π β (0...(β―βπ)) β¦ ((((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π)))) |
80 | 79 | oveq2d 7377 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (π Ξ£g (π β
(0...(β―βπ))
β¦ (((β―βπ)Cπ)πΉ((((β―βπ) β π)πΈ(πΌβ(π½ππ½))) Β· (π β π))))) = (π Ξ£g (π β
(0...(β―βπ))
β¦ ((((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))))) |
81 | 15, 80 | eqtrd 2773 |
1
β’ (((π β Fin β§ π
β CRing) β§ (π β π· β§ π½ β π β§ βπ β π (πππ) = (π½ππ½))) β (πΆβπ) = (π Ξ£g (π β
(0...(β―βπ))
β¦ ((((β―βπ)Cπ)π(((β―βπ) β π)πΈ(πΌβ(π½ππ½)))) Β· (π β π))))) |