Step | Hyp | Ref
| Expression |
1 | | cpmadugsum.a |
. . 3
β’ π΄ = (π Mat π
) |
2 | | cpmadugsum.b |
. . 3
β’ π΅ = (Baseβπ΄) |
3 | | cpmadugsum.p |
. . 3
β’ π = (Poly1βπ
) |
4 | | cpmadugsum.y |
. . 3
β’ π = (π Mat π) |
5 | | cpmadugsum.t |
. . 3
β’ π = (π matToPolyMat π
) |
6 | | cpmadugsum.x |
. . 3
β’ π = (var1βπ
) |
7 | | cpmadugsum.e |
. . 3
β’ β =
(.gβ(mulGrpβπ)) |
8 | | cpmadugsum.m |
. . 3
β’ Β· = (
Β·π βπ) |
9 | | cpmadugsum.r |
. . 3
β’ Γ =
(.rβπ) |
10 | | cpmadugsum.1 |
. . 3
β’ 1 =
(1rβπ) |
11 | | cpmadugsum.g |
. . 3
β’ + =
(+gβπ) |
12 | | cpmadugsum.s |
. . 3
β’ β =
(-gβπ) |
13 | | cpmadugsum.i |
. . 3
β’ πΌ = ((π Β· 1 ) β (πβπ)) |
14 | | cpmadugsum.j |
. . 3
β’ π½ = (π maAdju π) |
15 | | cpmadugsum.0 |
. . 3
β’ 0 =
(0gβπ) |
16 | | cpmadugsum.g2 |
. . 3
β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16 | cpmadugsum 22250 |
. 2
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) |
18 | | crngring 19984 |
. . . . . . . . . . . . 13
β’ (π
β CRing β π
β Ring) |
19 | 18 | anim2i 618 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β CRing) β (π β Fin β§ π
β Ring)) |
20 | 19 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β Fin β§ π
β Ring)) |
21 | 3, 4 | pmatring 22064 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β π β Ring) |
22 | | ringgrp 19977 |
. . . . . . . . . . 11
β’ (π β Ring β π β Grp) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π β Grp) |
24 | 3, 4 | pmatlmod 22065 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
25 | 18, 24 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β CRing) β π β LMod) |
26 | 18 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β CRing) β π
β Ring) |
27 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ) =
(Baseβπ) |
28 | 6, 3, 27 | vr1cl 21611 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π β (Baseβπ)) |
29 | 26, 28 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β CRing) β π β (Baseβπ)) |
30 | 3 | ply1crng 21592 |
. . . . . . . . . . . . . . 15
β’ (π
β CRing β π β CRing) |
31 | 4 | matsca2 21792 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π β CRing) β π = (Scalarβπ)) |
32 | 30, 31 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β CRing) β π = (Scalarβπ)) |
33 | 32 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β CRing) β
(Baseβπ) =
(Baseβ(Scalarβπ))) |
34 | 29, 33 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β CRing) β π β
(Baseβ(Scalarβπ))) |
35 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
36 | 35, 10 | ringidcl 19997 |
. . . . . . . . . . . . 13
β’ (π β Ring β 1 β
(Baseβπ)) |
37 | 19, 21, 36 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β CRing) β 1 β
(Baseβπ)) |
38 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Scalarβπ) =
(Scalarβπ) |
39 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
40 | 35, 38, 8, 39 | lmodvscl 20383 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ 1 β (Baseβπ)) β (π Β· 1 ) β (Baseβπ)) |
41 | 25, 34, 37, 40 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing) β (π Β· 1 ) β (Baseβπ)) |
42 | 41 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π Β· 1 ) β (Baseβπ)) |
43 | 5, 1, 2, 3, 4 | mat2pmatbas 22098 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β (Baseβπ)) |
44 | 18, 43 | syl3an2 1165 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (πβπ) β (Baseβπ)) |
45 | 35, 12 | grpsubcl 18835 |
. . . . . . . . . 10
β’ ((π β Grp β§ (π Β· 1 ) β (Baseβπ) β§ (πβπ) β (Baseβπ)) β ((π Β· 1 ) β (πβπ)) β (Baseβπ)) |
46 | 23, 42, 44, 45 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β ((π Β· 1 ) β (πβπ)) β (Baseβπ)) |
47 | 30 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π β CRing) |
48 | | eqid 2733 |
. . . . . . . . . 10
β’ (π maDet π) = (π maDet π) |
49 | 4, 35, 14, 48, 10, 9, 8 | madurid 22016 |
. . . . . . . . 9
β’ ((((π Β· 1 ) β (πβπ)) β (Baseβπ) β§ π β CRing) β (((π Β· 1 ) β (πβπ)) Γ (π½β((π Β· 1 ) β (πβπ)))) = (((π maDet π)β((π Β· 1 ) β (πβπ))) Β· 1 )) |
50 | 46, 47, 49 | syl2anc 585 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (((π Β· 1 ) β (πβπ)) Γ (π½β((π Β· 1 ) β (πβπ)))) = (((π maDet π)β((π Β· 1 ) β (πβπ))) Β· 1 )) |
51 | | id 22 |
. . . . . . . . . 10
β’ (πΌ = ((π Β· 1 ) β (πβπ)) β πΌ = ((π Β· 1 ) β (πβπ))) |
52 | | fveq2 6846 |
. . . . . . . . . 10
β’ (πΌ = ((π Β· 1 ) β (πβπ)) β (π½βπΌ) = (π½β((π Β· 1 ) β (πβπ)))) |
53 | 51, 52 | oveq12d 7379 |
. . . . . . . . 9
β’ (πΌ = ((π Β· 1 ) β (πβπ)) β (πΌ Γ (π½βπΌ)) = (((π Β· 1 ) β (πβπ)) Γ (π½β((π Β· 1 ) β (πβπ))))) |
54 | 13, 53 | mp1i 13 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (πΌ Γ (π½βπΌ)) = (((π Β· 1 ) β (πβπ)) Γ (π½β((π Β· 1 ) β (πβπ))))) |
55 | | cpmidgsum2.h |
. . . . . . . . 9
β’ π» = (πΎ Β· 1 ) |
56 | | cpmidgsum2.k |
. . . . . . . . . . 11
β’ πΎ = (πΆβπ) |
57 | | cpmidgsum2.c |
. . . . . . . . . . . 12
β’ πΆ = (π CharPlyMat π
) |
58 | 57, 1, 2, 3, 4, 48,
12, 6, 8, 5, 10 | chpmatval 22203 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (πΆβπ) = ((π maDet π)β((π Β· 1 ) β (πβπ)))) |
59 | 56, 58 | eqtrid 2785 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΎ = ((π maDet π)β((π Β· 1 ) β (πβπ)))) |
60 | 59 | oveq1d 7376 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (πΎ Β· 1 ) = (((π maDet π)β((π Β· 1 ) β (πβπ))) Β· 1 )) |
61 | 55, 60 | eqtrid 2785 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π» = (((π maDet π)β((π Β· 1 ) β (πβπ))) Β· 1 )) |
62 | 50, 54, 61 | 3eqtr4rd 2784 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π» = (πΌ Γ (π½βπΌ))) |
63 | 62 | adantr 482 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) β π» = (πΌ Γ (π½βπΌ))) |
64 | | simpr 486 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) β (πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) |
65 | 63, 64 | eqtrd 2773 |
. . . . 5
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) β π» = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) |
66 | 65 | ex 414 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β ((πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ)))) β π» = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ)))))) |
67 | 66 | reximdv 3164 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (βπ β (π΅ βm (0...π ))(πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ)))) β βπ β (π΅ βm (0...π ))π» = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ)))))) |
68 | 67 | reximdv 3164 |
. 2
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (βπ β β βπ β (π΅ βm (0...π ))(πΌ Γ (π½βπΌ)) = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ)))) β βπ β β βπ β (π΅ βm (0...π ))π» = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ)))))) |
69 | 17, 68 | mpd 15 |
1
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))π» = (π Ξ£g (π β β0
β¦ ((π β π) Β· (πΊβπ))))) |