Step | Hyp | Ref
| Expression |
1 | | cpmidpmat.g |
. 2
β’ πΊ = (π β β0 β¦
(((coe1βπΎ)βπ) β π)) |
2 | | fvexd 6861 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (0gβπ΄) β V) |
3 | | ovexd 7396 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
(((coe1βπΎ)βπ) β π) β V) |
4 | | fveq2 6846 |
. . . 4
β’ (π = π β ((coe1βπΎ)βπ) = ((coe1βπΎ)βπ)) |
5 | 4 | oveq1d 7376 |
. . 3
β’ (π = π β (((coe1βπΎ)βπ) β π) = (((coe1βπΎ)βπ) β π)) |
6 | | fvexd 6861 |
. . . . 5
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (0gβπ
) β V) |
7 | | cpmidgsum.k |
. . . . . . 7
β’ πΎ = (πΆβπ) |
8 | | cpmidgsum.c |
. . . . . . . 8
β’ πΆ = (π CharPlyMat π
) |
9 | | cpmidgsum.a |
. . . . . . . 8
β’ π΄ = (π Mat π
) |
10 | | cpmidgsum.b |
. . . . . . . 8
β’ π΅ = (Baseβπ΄) |
11 | | cpmidgsum.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
13 | 8, 9, 10, 11, 12 | chpmatply1 22204 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (πΆβπ) β (Baseβπ)) |
14 | 7, 13 | eqeltrid 2838 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΎ β (Baseβπ)) |
15 | | eqid 2733 |
. . . . . . 7
β’
(coe1βπΎ) = (coe1βπΎ) |
16 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
17 | 15, 12, 11, 16 | coe1fvalcl 21606 |
. . . . . 6
β’ ((πΎ β (Baseβπ) β§ π β β0) β
((coe1βπΎ)βπ) β (Baseβπ
)) |
18 | 14, 17 | sylan 581 |
. . . . 5
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
((coe1βπΎ)βπ) β (Baseβπ
)) |
19 | | crngring 19984 |
. . . . . . 7
β’ (π
β CRing β π
β Ring) |
20 | 19 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π
β Ring) |
21 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
22 | 11, 12, 21 | mptcoe1fsupp 21609 |
. . . . . 6
β’ ((π
β Ring β§ πΎ β (Baseβπ)) β (π β β0 β¦
((coe1βπΎ)βπ)) finSupp (0gβπ
)) |
23 | 20, 14, 22 | syl2anc 585 |
. . . . 5
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β β0 β¦
((coe1βπΎ)βπ)) finSupp (0gβπ
)) |
24 | 6, 18, 23 | mptnn0fsuppr 13913 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β0 βπ β β0
(π < π β β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
))) |
25 | | csbfv 6896 |
. . . . . . . . . . . . . 14
β’
β¦π /
πβ¦((coe1βπΎ)βπ) = ((coe1βπΎ)βπ) |
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
β¦π / πβ¦((coe1βπΎ)βπ) = ((coe1βπΎ)βπ)) |
27 | 26 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
(β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
) β ((coe1βπΎ)βπ) = (0gβπ
))) |
28 | 27 | biimpa 478 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β ((coe1βπΎ)βπ) = (0gβπ
)) |
29 | 9 | matsca2 21792 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β CRing) β π
= (Scalarβπ΄)) |
30 | 29 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π
= (Scalarβπ΄)) |
31 | 30 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β π
= (Scalarβπ΄)) |
32 | 31 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β (0gβπ
) =
(0gβ(Scalarβπ΄))) |
33 | 28, 32 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β ((coe1βπΎ)βπ) = (0gβ(Scalarβπ΄))) |
34 | 33 | oveq1d 7376 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β (((coe1βπΎ)βπ) β π) =
((0gβ(Scalarβπ΄)) β π)) |
35 | 9 | matlmod 21801 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β π΄ β LMod) |
36 | 19, 35 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β CRing) β π΄ β LMod) |
37 | 36 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π΄ β LMod) |
38 | 9 | matring 21815 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
39 | 19, 38 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β CRing) β π΄ β Ring) |
40 | | cpmidgsumm2pm.o |
. . . . . . . . . . . . . 14
β’ π = (1rβπ΄) |
41 | 10, 40 | ringidcl 19997 |
. . . . . . . . . . . . 13
β’ (π΄ β Ring β π β π΅) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β CRing) β π β π΅) |
43 | 42 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π β π΅) |
44 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
45 | | cpmidgsumm2pm.m |
. . . . . . . . . . . 12
β’ β = (
Β·π βπ΄) |
46 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβ(Scalarβπ΄)) =
(0gβ(Scalarβπ΄)) |
47 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβπ΄) = (0gβπ΄) |
48 | 10, 44, 45, 46, 47 | lmod0vs 20399 |
. . . . . . . . . . 11
β’ ((π΄ β LMod β§ π β π΅) β
((0gβ(Scalarβπ΄)) β π) = (0gβπ΄)) |
49 | 37, 43, 48 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β
((0gβ(Scalarβπ΄)) β π) = (0gβπ΄)) |
50 | 49 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β
((0gβ(Scalarβπ΄)) β π) = (0gβπ΄)) |
51 | 34, 50 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β (((coe1βπΎ)βπ) β π) = (0gβπ΄)) |
52 | 51 | ex 414 |
. . . . . . 7
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
(β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
) β (((coe1βπΎ)βπ) β π) = (0gβπ΄))) |
53 | 52 | imim2d 57 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β ((π < π β β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β (π < π β (((coe1βπΎ)βπ) β π) = (0gβπ΄)))) |
54 | 53 | ralimdva 3161 |
. . . . 5
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (βπ β β0 (π < π β β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β βπ β β0 (π < π β (((coe1βπΎ)βπ) β π) = (0gβπ΄)))) |
55 | 54 | reximdv 3164 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (βπ β β0 βπ β β0
(π < π β β¦π / πβ¦((coe1βπΎ)βπ) = (0gβπ
)) β βπ β β0 βπ β β0
(π < π β (((coe1βπΎ)βπ) β π) = (0gβπ΄)))) |
56 | 24, 55 | mpd 15 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β0 βπ β β0
(π < π β (((coe1βπΎ)βπ) β π) = (0gβπ΄))) |
57 | 2, 3, 5, 56 | mptnn0fsuppd 13912 |
. 2
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β β0 β¦
(((coe1βπΎ)βπ) β π)) finSupp (0gβπ΄)) |
58 | 1, 57 | eqbrtrid 5144 |
1
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΊ finSupp (0gβπ΄)) |