Step | Hyp | Ref
| Expression |
1 | | fvexd 6861 |
. 2
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (0gβπ) β V) |
2 | | ovexd 7396 |
. 2
β’ (((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β ((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) β V) |
3 | | ply1mulgsum.p |
. . . 4
β’ π = (Poly1βπ
) |
4 | | ply1mulgsum.b |
. . . 4
β’ π΅ = (Baseβπ) |
5 | | ply1mulgsum.a |
. . . 4
β’ π΄ = (coe1βπΎ) |
6 | | ply1mulgsum.c |
. . . 4
β’ πΆ = (coe1βπΏ) |
7 | | ply1mulgsum.x |
. . . 4
β’ π = (var1βπ
) |
8 | | ply1mulgsum.pm |
. . . 4
β’ Γ =
(.rβπ) |
9 | | ply1mulgsum.sm |
. . . 4
β’ Β· = (
Β·π βπ) |
10 | | ply1mulgsum.rm |
. . . 4
β’ β =
(.rβπ
) |
11 | | ply1mulgsum.m |
. . . 4
β’ π = (mulGrpβπ) |
12 | | ply1mulgsum.e |
. . . 4
β’ β =
(.gβπ) |
13 | 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | ply1mulgsumlem2 46558 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β βπ β β0 βπ β β0
(π < π β (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
))) |
14 | | vex 3451 |
. . . . . . . . 9
β’ π β V |
15 | | csbov12g 7405 |
. . . . . . . . . 10
β’ (π β V β
β¦π / πβ¦((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (β¦π / πβ¦(π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β·
β¦π / πβ¦(π β π))) |
16 | | csbov2g 7407 |
. . . . . . . . . . . 12
β’ (π β V β
β¦π / πβ¦(π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (π
Ξ£g
β¦π / πβ¦(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))))) |
17 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π β V β π β V) |
18 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (0...π) = (0...π)) |
19 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΆβ(π β π)) = (πΆβ(π β π))) |
20 | 19 | oveq2d 7377 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π΄βπ) β (πΆβ(π β π))) = ((π΄βπ) β (πΆβ(π β π)))) |
21 | 18, 20 | mpteq12dv 5200 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))) = (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β V β§ π = π) β (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))) = (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) |
23 | 17, 22 | csbied 3897 |
. . . . . . . . . . . . 13
β’ (π β V β
β¦π / πβ¦(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))) = (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) |
24 | 23 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (π β V β (π
Ξ£g
β¦π / πβ¦(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))))) |
25 | 16, 24 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β V β
β¦π / πβ¦(π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π)))))) |
26 | | csbov1g 7406 |
. . . . . . . . . . . 12
β’ (π β V β
β¦π / πβ¦(π β π) = (β¦π / πβ¦π β π)) |
27 | | csbvarg 4395 |
. . . . . . . . . . . . 13
β’ (π β V β
β¦π / πβ¦π = π) |
28 | 27 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ (π β V β
(β¦π / πβ¦π β π) = (π β π)) |
29 | 26, 28 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β V β
β¦π / πβ¦(π β π) = (π β π)) |
30 | 25, 29 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π β V β
(β¦π / πβ¦(π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β·
β¦π / πβ¦(π β π)) = ((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π))) |
31 | 15, 30 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β V β
β¦π / πβ¦((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = ((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π))) |
32 | 14, 31 | ax-mp 5 |
. . . . . . . 8
β’
β¦π /
πβ¦((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = ((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) |
33 | | oveq1 7368 |
. . . . . . . . 9
β’ ((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
) β ((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = ((0gβπ
) Β· (π β π))) |
34 | 3 | ply1sca 21647 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π
= (Scalarβπ)) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β π
= (Scalarβπ)) |
36 | 35 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β π
=
(Scalarβπ)) |
37 | 36 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β (0gβπ
) = (0gβ(Scalarβπ))) |
38 | 37 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β ((0gβπ
) Β· (π β π)) =
((0gβ(Scalarβπ)) Β· (π β π))) |
39 | 3 | ply1lmod 21646 |
. . . . . . . . . . . . 13
β’ (π
β Ring β π β LMod) |
40 | 39 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β π β LMod) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β π β
LMod) |
42 | 11, 4 | mgpbas 19910 |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
43 | 3 | ply1ring 21642 |
. . . . . . . . . . . . . . 15
β’ (π
β Ring β π β Ring) |
44 | 11 | ringmgp 19978 |
. . . . . . . . . . . . . . 15
β’ (π β Ring β π β Mnd) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π β Mnd) |
46 | 45 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β π β Mnd) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β π β
Mnd) |
48 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β π β
β0) |
49 | 7, 3, 4 | vr1cl 21611 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π β π΅) |
50 | 49 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β π β π΅) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β π β π΅) |
52 | 42, 12, 47, 48, 51 | mulgnn0cld 18905 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β (π β π) β π΅) |
53 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Scalarβπ) =
(Scalarβπ) |
54 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
55 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
56 | 4, 53, 9, 54, 55 | lmod0vs 20399 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (π β π) β π΅) β
((0gβ(Scalarβπ)) Β· (π β π)) = (0gβπ)) |
57 | 41, 52, 56 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β ((0gβ(Scalarβπ)) Β· (π β π)) = (0gβπ)) |
58 | 38, 57 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β ((0gβπ
) Β· (π β π)) = (0gβπ)) |
59 | 33, 58 | sylan9eqr 2795 |
. . . . . . . 8
β’
(((((π
β Ring
β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β§ (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
)) β ((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ)) |
60 | 32, 59 | eqtrid 2785 |
. . . . . . 7
β’
(((((π
β Ring
β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β§ (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
)) β β¦π / πβ¦((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ)) |
61 | 60 | ex 414 |
. . . . . 6
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β ((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
) β β¦π / πβ¦((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ))) |
62 | 61 | imim2d 57 |
. . . . 5
β’ ((((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β§ π β β0)
β ((π < π β (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
)) β (π < π β β¦π / πβ¦((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ)))) |
63 | 62 | ralimdva 3161 |
. . . 4
β’ (((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β§ π β β0) β
(βπ β
β0 (π <
π β (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
)) β βπ β β0
(π < π β β¦π / πβ¦((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ)))) |
64 | 63 | reximdva 3162 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (βπ β β0 βπ β β0
(π < π β (π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) = (0gβπ
)) β βπ β β0
βπ β
β0 (π <
π β
β¦π / πβ¦((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ)))) |
65 | 13, 64 | mpd 15 |
. 2
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β βπ β β0 βπ β β0
(π < π β β¦π / πβ¦((π
Ξ£g (π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π)) = (0gβπ))) |
66 | 1, 2, 65 | mptnn0fsupp 13911 |
1
β’ ((π
β Ring β§ πΎ β π΅ β§ πΏ β π΅) β (π β β0 β¦ ((π
Ξ£g
(π β (0...π) β¦ ((π΄βπ) β (πΆβ(π β π))))) Β· (π β π))) finSupp (0gβπ)) |