Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . 8
β’ π = (πΌ mPoly π
) |
2 | | mdegmulle2.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
3 | | eqid 2737 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
4 | | mdegmulle2.t |
. . . . . . . 8
β’ Β· =
(.rβπ) |
5 | | mdegmullem.a |
. . . . . . . 8
β’ π΄ = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
6 | | mdegmulle2.f |
. . . . . . . 8
β’ (π β πΉ β π΅) |
7 | | mdegmulle2.g |
. . . . . . . 8
β’ (π β πΊ β π΅) |
8 | 1, 2, 3, 4, 5, 6, 7 | mplmul 21431 |
. . . . . . 7
β’ (π β (πΉ Β· πΊ) = (π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))))))) |
9 | 8 | fveq1d 6849 |
. . . . . 6
β’ (π β ((πΉ Β· πΊ)βπ₯) = ((π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))))))βπ₯)) |
10 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β ((πΉ Β· πΊ)βπ₯) = ((π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))))))βπ₯)) |
11 | | breq2 5114 |
. . . . . . . . . 10
β’ (π = π₯ β (π βr β€ π β π βr β€ π₯)) |
12 | 11 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = π₯ β {π β π΄ β£ π βr β€ π} = {π β π΄ β£ π βr β€ π₯}) |
13 | | fvoveq1 7385 |
. . . . . . . . . 10
β’ (π = π₯ β (πΊβ(π βf β π)) = (πΊβ(π₯ βf β π))) |
14 | 13 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π₯ β ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))) = ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π)))) |
15 | 12, 14 | mpteq12dv 5201 |
. . . . . . . 8
β’ (π = π₯ β (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π)))) = (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))))) |
16 | 15 | oveq2d 7378 |
. . . . . . 7
β’ (π = π₯ β (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))))) = (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π)))))) |
17 | | eqid 2737 |
. . . . . . 7
β’ (π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π)))))) = (π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π)))))) |
18 | | ovex 7395 |
. . . . . . 7
β’ (π
Ξ£g
(π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))))) β V |
19 | 16, 17, 18 | fvmpt 6953 |
. . . . . 6
β’ (π₯ β π΄ β ((π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))))))βπ₯) = (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π)))))) |
20 | 19 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β ((π β π΄ β¦ (π
Ξ£g (π β {π β π΄ β£ π βr β€ π} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π βf β π))))))βπ₯) = (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π)))))) |
21 | | mdegaddle.d |
. . . . . . . . . . . . 13
β’ π· = (πΌ mDeg π
) |
22 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(0gβπ
) = (0gβπ
) |
23 | | mdegmullem.h |
. . . . . . . . . . . . 13
β’ π» = (π β π΄ β¦ (βfld
Ξ£g π)) |
24 | 6 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β πΉ β π΅) |
25 | | elrabi 3644 |
. . . . . . . . . . . . . . 15
β’ (π β {π β π΄ β£ π βr β€ π₯} β π β π΄) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π β π΄) |
27 | 26 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β π β π΄) |
28 | 21, 1, 2 | mdegxrcl 25448 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β π΅ β (π·βπΉ) β
β*) |
29 | 6, 28 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π·βπΉ) β
β*) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π·βπΉ) β
β*) |
31 | | nn0ssre 12424 |
. . . . . . . . . . . . . . . . . . 19
β’
β0 β β |
32 | | ressxr 11206 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β β* |
33 | 31, 32 | sstri 3958 |
. . . . . . . . . . . . . . . . . 18
β’
β0 β β* |
34 | | mdegmulle2.j1 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π½ β
β0) |
35 | 33, 34 | sselid 3947 |
. . . . . . . . . . . . . . . . 17
β’ (π β π½ β
β*) |
36 | 35 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π½ β
β*) |
37 | 5, 23 | tdeglem1 25436 |
. . . . . . . . . . . . . . . . . . 19
β’ π»:π΄βΆβ0 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π»:π΄βΆβ0) |
39 | 38, 26 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»βπ) β
β0) |
40 | 33, 39 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»βπ) β
β*) |
41 | 30, 36, 40 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((π·βπΉ) β β* β§ π½ β β*
β§ (π»βπ) β
β*)) |
42 | 41 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β ((π·βπΉ) β β* β§ π½ β β*
β§ (π»βπ) β
β*)) |
43 | | mdegmulle2.j2 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π·βπΉ) β€ π½) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π·βπΉ) β€ π½) |
45 | 44 | anim1i 616 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β§ π½ < (π»βπ)) β ((π·βπΉ) β€ π½ β§ π½ < (π»βπ))) |
46 | 45 | anasss 468 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β ((π·βπΉ) β€ π½ β§ π½ < (π»βπ))) |
47 | | xrlelttr 13082 |
. . . . . . . . . . . . . 14
β’ (((π·βπΉ) β β* β§ π½ β β*
β§ (π»βπ) β β*)
β (((π·βπΉ) β€ π½ β§ π½ < (π»βπ)) β (π·βπΉ) < (π»βπ))) |
48 | 42, 46, 47 | sylc 65 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β (π·βπΉ) < (π»βπ)) |
49 | 21, 1, 2, 22, 5, 23, 24, 27, 48 | mdeglt 25446 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β (πΉβπ) = (0gβπ
)) |
50 | 49 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) =
((0gβπ
)(.rβπ
)(πΊβ(π₯ βf β π)))) |
51 | | mdegaddle.r |
. . . . . . . . . . . . . 14
β’ (π β π
β Ring) |
52 | 51 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π
β Ring) |
53 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(Baseβπ
) =
(Baseβπ
) |
54 | 1, 53, 2, 5, 7 | mplelf 21420 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ:π΄βΆ(Baseβπ
)) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β πΊ:π΄βΆ(Baseβπ
)) |
56 | | ssrab2 4042 |
. . . . . . . . . . . . . . 15
β’ {π β π΄ β£ π βr β€ π₯} β π΄ |
57 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π₯ β π΄) |
58 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ {π β π΄ β£ π βr β€ π₯} = {π β π΄ β£ π βr β€ π₯} |
59 | 5, 58 | psrbagconcl 21352 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π΄ β§ π β {π β π΄ β£ π βr β€ π₯}) β (π₯ βf β π) β {π β π΄ β£ π βr β€ π₯}) |
60 | 57, 59 | sylancom 589 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π₯ βf β π) β {π β π΄ β£ π βr β€ π₯}) |
61 | 56, 60 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π₯ βf β π) β π΄) |
62 | 55, 61 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (πΊβ(π₯ βf β π)) β (Baseβπ
)) |
63 | 53, 3, 22 | ringlz 20018 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (πΊβ(π₯ βf β π)) β (Baseβπ
)) β
((0gβπ
)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
64 | 52, 62, 63 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((0gβπ
)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
65 | 64 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β ((0gβπ
)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
66 | 50, 65 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ π½ < (π»βπ))) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
67 | 66 | anassrs 469 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β§ π½ < (π»βπ)) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
68 | 7 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β πΊ β π΅) |
69 | 61 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β (π₯ βf β π) β π΄) |
70 | 21, 1, 2 | mdegxrcl 25448 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β π΅ β (π·βπΊ) β
β*) |
71 | 7, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π·βπΊ) β
β*) |
72 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π·βπΊ) β
β*) |
73 | | mdegmulle2.k1 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΎ β
β0) |
74 | 33, 73 | sselid 3947 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΎ β
β*) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β πΎ β
β*) |
76 | 38, 61 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»β(π₯ βf β π)) β
β0) |
77 | 33, 76 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»β(π₯ βf β π)) β
β*) |
78 | 72, 75, 77 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((π·βπΊ) β β* β§ πΎ β β*
β§ (π»β(π₯ βf β
π)) β
β*)) |
79 | 78 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β ((π·βπΊ) β β* β§ πΎ β β*
β§ (π»β(π₯ βf β
π)) β
β*)) |
80 | | mdegmulle2.k2 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π·βπΊ) β€ πΎ) |
81 | 80 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π·βπΊ) β€ πΎ) |
82 | 81 | anim1i 616 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β§ πΎ < (π»β(π₯ βf β π))) β ((π·βπΊ) β€ πΎ β§ πΎ < (π»β(π₯ βf β π)))) |
83 | 82 | anasss 468 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β ((π·βπΊ) β€ πΎ β§ πΎ < (π»β(π₯ βf β π)))) |
84 | | xrlelttr 13082 |
. . . . . . . . . . . . . 14
β’ (((π·βπΊ) β β* β§ πΎ β β*
β§ (π»β(π₯ βf β
π)) β
β*) β (((π·βπΊ) β€ πΎ β§ πΎ < (π»β(π₯ βf β π))) β (π·βπΊ) < (π»β(π₯ βf β π)))) |
85 | 79, 83, 84 | sylc 65 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β (π·βπΊ) < (π»β(π₯ βf β π))) |
86 | 21, 1, 2, 22, 5, 23, 68, 69, 85 | mdeglt 25446 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β (πΊβ(π₯ βf β π)) = (0gβπ
)) |
87 | 86 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) = ((πΉβπ)(.rβπ
)(0gβπ
))) |
88 | 1, 53, 2, 5, 6 | mplelf 21420 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆ(Baseβπ
)) |
89 | 88 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β πΉ:π΄βΆ(Baseβπ
)) |
90 | 89, 26 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (πΉβπ) β (Baseβπ
)) |
91 | 53, 3, 22 | ringrz 20019 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (πΉβπ) β (Baseβπ
)) β ((πΉβπ)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
92 | 52, 90, 91 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((πΉβπ)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
93 | 92 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β ((πΉβπ)(.rβπ
)(0gβπ
)) = (0gβπ
)) |
94 | 87, 93 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ (π β {π β π΄ β£ π βr β€ π₯} β§ πΎ < (π»β(π₯ βf β π)))) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
95 | 94 | anassrs 469 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β§ πΎ < (π»β(π₯ βf β π))) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
96 | | simplrr 777 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π½ + πΎ) < (π»βπ₯)) |
97 | 39 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»βπ) β β) |
98 | 76 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»β(π₯ βf β π)) β
β) |
99 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π½ β
β0) |
100 | 99 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β π½ β β) |
101 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β πΎ β
β0) |
102 | 101 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β πΎ β β) |
103 | | le2add 11644 |
. . . . . . . . . . . . 13
β’ ((((π»βπ) β β β§ (π»β(π₯ βf β π)) β β) β§ (π½ β β β§ πΎ β β)) β
(((π»βπ) β€ π½ β§ (π»β(π₯ βf β π)) β€ πΎ) β ((π»βπ) + (π»β(π₯ βf β π))) β€ (π½ + πΎ))) |
104 | 97, 98, 100, 102, 103 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (((π»βπ) β€ π½ β§ (π»β(π₯ βf β π)) β€ πΎ) β ((π»βπ) + (π»β(π₯ βf β π))) β€ (π½ + πΎ))) |
105 | 5, 23 | tdeglem3 25438 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ (π₯ βf β π) β π΄) β (π»β(π βf + (π₯ βf β π))) = ((π»βπ) + (π»β(π₯ βf β π)))) |
106 | 26, 61, 105 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»β(π βf + (π₯ βf β π))) = ((π»βπ) + (π»β(π₯ βf β π)))) |
107 | | mdegaddle.i |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β π) |
108 | 107 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β πΌ β π) |
109 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΄ β π:πΌβΆβ0) |
110 | 109 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β π:πΌβΆβ0) |
111 | 110 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β (πβπ) β
β0) |
112 | 111 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β (πβπ) β β) |
113 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β π΄ β π₯:πΌβΆβ0) |
114 | 113 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β π₯:πΌβΆβ0) |
115 | 114 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β (π₯βπ) β
β0) |
116 | 115 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β (π₯βπ) β β) |
117 | 112, 116 | pncan3d 11522 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β ((πβπ) + ((π₯βπ) β (πβπ))) = (π₯βπ)) |
118 | 117 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β (π β πΌ β¦ ((πβπ) + ((π₯βπ) β (πβπ)))) = (π β πΌ β¦ (π₯βπ))) |
119 | | simp1 1137 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β πΌ β π) |
120 | | fvexd 6862 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β (πβπ) β V) |
121 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β ((π₯βπ) β (πβπ)) β V) |
122 | 110 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β π = (π β πΌ β¦ (πβπ))) |
123 | | fvexd 6862 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΌ β π β§ π β π΄ β§ π₯ β π΄) β§ π β πΌ) β (π₯βπ) β V) |
124 | 114 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β π₯ = (π β πΌ β¦ (π₯βπ))) |
125 | 119, 123,
120, 124, 122 | offval2 7642 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β (π₯ βf β π) = (π β πΌ β¦ ((π₯βπ) β (πβπ)))) |
126 | 119, 120,
121, 122, 125 | offval2 7642 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β (π βf + (π₯ βf β π)) = (π β πΌ β¦ ((πβπ) + ((π₯βπ) β (πβπ))))) |
127 | 118, 126,
124 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β π β§ π β π΄ β§ π₯ β π΄) β (π βf + (π₯ βf β π)) = π₯) |
128 | 108, 26, 57, 127 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π βf + (π₯ βf β π)) = π₯) |
129 | 128 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»β(π βf + (π₯ βf β π))) = (π»βπ₯)) |
130 | 106, 129 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((π»βπ) + (π»β(π₯ βf β π))) = (π»βπ₯)) |
131 | 130 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (((π»βπ) + (π»β(π₯ βf β π))) β€ (π½ + πΎ) β (π»βπ₯) β€ (π½ + πΎ))) |
132 | 104, 131 | sylibd 238 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (((π»βπ) β€ π½ β§ (π»β(π₯ βf β π)) β€ πΎ) β (π»βπ₯) β€ (π½ + πΎ))) |
133 | 97, 100 | lenltd 11308 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((π»βπ) β€ π½ β Β¬ π½ < (π»βπ))) |
134 | 98, 102 | lenltd 11308 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((π»β(π₯ βf β π)) β€ πΎ β Β¬ πΎ < (π»β(π₯ βf β π)))) |
135 | 133, 134 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (((π»βπ) β€ π½ β§ (π»β(π₯ βf β π)) β€ πΎ) β (Β¬ π½ < (π»βπ) β§ Β¬ πΎ < (π»β(π₯ βf β π))))) |
136 | | ioran 983 |
. . . . . . . . . . . 12
β’ (Β¬
(π½ < (π»βπ) β¨ πΎ < (π»β(π₯ βf β π))) β (Β¬ π½ < (π»βπ) β§ Β¬ πΎ < (π»β(π₯ βf β π)))) |
137 | 135, 136 | bitr4di 289 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (((π»βπ) β€ π½ β§ (π»β(π₯ βf β π)) β€ πΎ) β Β¬ (π½ < (π»βπ) β¨ πΎ < (π»β(π₯ βf β π))))) |
138 | 38, 57 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»βπ₯) β
β0) |
139 | 138 | nn0red 12481 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π»βπ₯) β β) |
140 | 34, 73 | nn0addcld 12484 |
. . . . . . . . . . . . . 14
β’ (π β (π½ + πΎ) β
β0) |
141 | 140 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π½ + πΎ) β
β0) |
142 | 141 | nn0red 12481 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π½ + πΎ) β β) |
143 | 139, 142 | lenltd 11308 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((π»βπ₯) β€ (π½ + πΎ) β Β¬ (π½ + πΎ) < (π»βπ₯))) |
144 | 132, 137,
143 | 3imtr3d 293 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (Β¬ (π½ < (π»βπ) β¨ πΎ < (π»β(π₯ βf β π))) β Β¬ (π½ + πΎ) < (π»βπ₯))) |
145 | 96, 144 | mt4d 117 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β (π½ < (π»βπ) β¨ πΎ < (π»β(π₯ βf β π)))) |
146 | 67, 95, 145 | mpjaodan 958 |
. . . . . . . 8
β’ (((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β§ π β {π β π΄ β£ π βr β€ π₯}) β ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))) = (0gβπ
)) |
147 | 146 | mpteq2dva 5210 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π)))) = (π β {π β π΄ β£ π βr β€ π₯} β¦ (0gβπ
))) |
148 | 147 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))))) = (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ (0gβπ
)))) |
149 | | ringmnd 19981 |
. . . . . . . . 9
β’ (π
β Ring β π
β Mnd) |
150 | 51, 149 | syl 17 |
. . . . . . . 8
β’ (π β π
β Mnd) |
151 | 150 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β π
β Mnd) |
152 | | ovex 7395 |
. . . . . . . 8
β’
(β0 βm πΌ) β V |
153 | 5, 152 | rab2ex 5297 |
. . . . . . 7
β’ {π β π΄ β£ π βr β€ π₯} β V |
154 | 22 | gsumz 18653 |
. . . . . . 7
β’ ((π
β Mnd β§ {π β π΄ β£ π βr β€ π₯} β V) β (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ (0gβπ
))) = (0gβπ
)) |
155 | 151, 153,
154 | sylancl 587 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ (0gβπ
))) = (0gβπ
)) |
156 | 148, 155 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β (π
Ξ£g (π β {π β π΄ β£ π βr β€ π₯} β¦ ((πΉβπ)(.rβπ
)(πΊβ(π₯ βf β π))))) =
(0gβπ
)) |
157 | 10, 20, 156 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ (π₯ β π΄ β§ (π½ + πΎ) < (π»βπ₯))) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
)) |
158 | 157 | expr 458 |
. . 3
β’ ((π β§ π₯ β π΄) β ((π½ + πΎ) < (π»βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
))) |
159 | 158 | ralrimiva 3144 |
. 2
β’ (π β βπ₯ β π΄ ((π½ + πΎ) < (π»βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
))) |
160 | 1 | mplring 21440 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
161 | 107, 51, 160 | syl2anc 585 |
. . . 4
β’ (π β π β Ring) |
162 | 2, 4 | ringcl 19988 |
. . . 4
β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ Β· πΊ) β π΅) |
163 | 161, 6, 7, 162 | syl3anc 1372 |
. . 3
β’ (π β (πΉ Β· πΊ) β π΅) |
164 | 33, 140 | sselid 3947 |
. . 3
β’ (π β (π½ + πΎ) β
β*) |
165 | 21, 1, 2, 22, 5, 23 | mdegleb 25445 |
. . 3
β’ (((πΉ Β· πΊ) β π΅ β§ (π½ + πΎ) β β*) β ((π·β(πΉ Β· πΊ)) β€ (π½ + πΎ) β βπ₯ β π΄ ((π½ + πΎ) < (π»βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
)))) |
166 | 163, 164,
165 | syl2anc 585 |
. 2
β’ (π β ((π·β(πΉ Β· πΊ)) β€ (π½ + πΎ) β βπ₯ β π΄ ((π½ + πΎ) < (π»βπ₯) β ((πΉ Β· πΊ)βπ₯) = (0gβπ
)))) |
167 | 159, 166 | mpbird 257 |
1
β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) |