Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . 3
β’
(Poly1β(opprβπ
)) =
(Poly1β(opprβπ
)) |
2 | | ply1divalg.d |
. . . 4
β’ π· = ( deg1
βπ
) |
3 | | eqidd 2733 |
. . . . . 6
β’ (β€
β (Baseβπ
) =
(Baseβπ
)) |
4 | | eqid 2732 |
. . . . . . . 8
β’
(opprβπ
) = (opprβπ
) |
5 | | eqid 2732 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
6 | 4, 5 | opprbas 20149 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβ(opprβπ
)) |
7 | 6 | a1i 11 |
. . . . . 6
β’ (β€
β (Baseβπ
) =
(Baseβ(opprβπ
))) |
8 | | eqid 2732 |
. . . . . . . . 9
β’
(+gβπ
) = (+gβπ
) |
9 | 4, 8 | oppradd 20151 |
. . . . . . . 8
β’
(+gβπ
) =
(+gβ(opprβπ
)) |
10 | 9 | oveqi 7418 |
. . . . . . 7
β’ (π(+gβπ
)π) = (π(+gβ(opprβπ
))π) |
11 | 10 | a1i 11 |
. . . . . 6
β’
((β€ β§ (π
β (Baseβπ
) β§
π β (Baseβπ
))) β (π(+gβπ
)π) = (π(+gβ(opprβπ
))π)) |
12 | 3, 7, 11 | deg1propd 25595 |
. . . . 5
β’ (β€
β ( deg1 βπ
) = ( deg1
β(opprβπ
))) |
13 | 12 | mptru 1548 |
. . . 4
β’ (
deg1 βπ
) =
( deg1 β(opprβπ
)) |
14 | 2, 13 | eqtri 2760 |
. . 3
β’ π· = ( deg1
β(opprβπ
)) |
15 | | ply1divalg.b |
. . . 4
β’ π΅ = (Baseβπ) |
16 | | ply1divalg.p |
. . . . . 6
β’ π = (Poly1βπ
) |
17 | 16 | fveq2i 6891 |
. . . . 5
β’
(Baseβπ) =
(Baseβ(Poly1βπ
)) |
18 | 3, 7, 11 | ply1baspropd 21756 |
. . . . . 6
β’ (β€
β (Baseβ(Poly1βπ
)) =
(Baseβ(Poly1β(opprβπ
)))) |
19 | 18 | mptru 1548 |
. . . . 5
β’
(Baseβ(Poly1βπ
)) =
(Baseβ(Poly1β(opprβπ
))) |
20 | 17, 19 | eqtri 2760 |
. . . 4
β’
(Baseβπ) =
(Baseβ(Poly1β(opprβπ
))) |
21 | 15, 20 | eqtri 2760 |
. . 3
β’ π΅ =
(Baseβ(Poly1β(opprβπ
))) |
22 | | ply1divalg.m |
. . . 4
β’ β =
(-gβπ) |
23 | 20 | a1i 11 |
. . . . . 6
β’ (β€
β (Baseβπ) =
(Baseβ(Poly1β(opprβπ
)))) |
24 | 16 | fveq2i 6891 |
. . . . . . . 8
β’
(+gβπ) =
(+gβ(Poly1βπ
)) |
25 | 3, 7, 11 | ply1plusgpropd 21757 |
. . . . . . . . 9
β’ (β€
β (+gβ(Poly1βπ
)) =
(+gβ(Poly1β(opprβπ
)))) |
26 | 25 | mptru 1548 |
. . . . . . . 8
β’
(+gβ(Poly1βπ
)) =
(+gβ(Poly1β(opprβπ
))) |
27 | 24, 26 | eqtri 2760 |
. . . . . . 7
β’
(+gβπ) =
(+gβ(Poly1β(opprβπ
))) |
28 | 27 | a1i 11 |
. . . . . 6
β’ (β€
β (+gβπ) =
(+gβ(Poly1β(opprβπ
)))) |
29 | 23, 28 | grpsubpropd 18924 |
. . . . 5
β’ (β€
β (-gβπ) =
(-gβ(Poly1β(opprβπ
)))) |
30 | 29 | mptru 1548 |
. . . 4
β’
(-gβπ) =
(-gβ(Poly1β(opprβπ
))) |
31 | 22, 30 | eqtri 2760 |
. . 3
β’ β =
(-gβ(Poly1β(opprβπ
))) |
32 | | ply1divalg.z |
. . . 4
β’ 0 =
(0gβπ) |
33 | 15 | a1i 11 |
. . . . . 6
β’ (β€
β π΅ =
(Baseβπ)) |
34 | 21 | a1i 11 |
. . . . . 6
β’ (β€
β π΅ =
(Baseβ(Poly1β(opprβπ
)))) |
35 | 27 | oveqi 7418 |
. . . . . . 7
β’ (π(+gβπ)π) = (π(+gβ(Poly1β(opprβπ
)))π) |
36 | 35 | a1i 11 |
. . . . . 6
β’
((β€ β§ (π
β π΅ β§ π β π΅)) β (π(+gβπ)π) = (π(+gβ(Poly1β(opprβπ
)))π)) |
37 | 33, 34, 36 | grpidpropd 18577 |
. . . . 5
β’ (β€
β (0gβπ) =
(0gβ(Poly1β(opprβπ
)))) |
38 | 37 | mptru 1548 |
. . . 4
β’
(0gβπ) =
(0gβ(Poly1β(opprβπ
))) |
39 | 32, 38 | eqtri 2760 |
. . 3
β’ 0 =
(0gβ(Poly1β(opprβπ
))) |
40 | | eqid 2732 |
. . 3
β’
(.rβ(Poly1β(opprβπ
))) =
(.rβ(Poly1β(opprβπ
))) |
41 | | ply1divalg.r1 |
. . . 4
β’ (π β π
β Ring) |
42 | 4 | opprring 20153 |
. . . 4
β’ (π
β Ring β
(opprβπ
) β Ring) |
43 | 41, 42 | syl 17 |
. . 3
β’ (π β
(opprβπ
) β Ring) |
44 | | ply1divalg.f |
. . 3
β’ (π β πΉ β π΅) |
45 | | ply1divalg.g1 |
. . 3
β’ (π β πΊ β π΅) |
46 | | ply1divalg.g2 |
. . 3
β’ (π β πΊ β 0 ) |
47 | | ply1divalg.g3 |
. . 3
β’ (π β
((coe1βπΊ)β(π·βπΊ)) β π) |
48 | | ply1divalg.u |
. . . 4
β’ π = (Unitβπ
) |
49 | 48, 4 | opprunit 20183 |
. . 3
β’ π =
(Unitβ(opprβπ
)) |
50 | 1, 14, 21, 31, 39, 40, 43, 44, 45, 46, 47, 49 | ply1divalg 25646 |
. 2
β’ (π β β!π β π΅ (π·β(πΉ β (πΊ(.rβ(Poly1β(opprβπ
)))π))) <
(π·βπΊ)) |
51 | 41 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π΅) β π
β Ring) |
52 | 45 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π΅) β πΊ β π΅) |
53 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π β π΅) β π β π΅) |
54 | | ply1divalg.t |
. . . . . . . . 9
β’ β =
(.rβπ) |
55 | 16, 4, 1, 54, 40, 15 | ply1opprmul 21752 |
. . . . . . . 8
β’ ((π
β Ring β§ πΊ β π΅ β§ π β π΅) β (πΊ(.rβ(Poly1β(opprβπ
)))π) = (π β πΊ)) |
56 | 51, 52, 53, 55 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ π β π΅) β (πΊ(.rβ(Poly1β(opprβπ
)))π) = (π β πΊ)) |
57 | 56 | eqcomd 2738 |
. . . . . 6
β’ ((π β§ π β π΅) β (π β πΊ) = (πΊ(.rβ(Poly1β(opprβπ
)))π)) |
58 | 57 | oveq2d 7421 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉ β (π β πΊ)) = (πΉ β (πΊ(.rβ(Poly1β(opprβπ
)))π))) |
59 | 58 | fveq2d 6892 |
. . . 4
β’ ((π β§ π β π΅) β (π·β(πΉ β (π β πΊ))) = (π·β(πΉ β (πΊ(.rβ(Poly1β(opprβπ
)))π)))) |
60 | 59 | breq1d 5157 |
. . 3
β’ ((π β§ π β π΅) β ((π·β(πΉ β (π β πΊ))) < (π·βπΊ) β (π·β(πΉ β (πΊ(.rβ(Poly1β(opprβπ
)))π))) <
(π·βπΊ))) |
61 | 60 | reubidva 3392 |
. 2
β’ (π β (β!π β π΅ (π·β(πΉ β (π β πΊ))) < (π·βπΊ) β β!π β π΅ (π·β(πΉ β (πΊ(.rβ(Poly1β(opprβπ
)))π))) <
(π·βπΊ))) |
62 | 50, 61 | mpbird 256 |
1
β’ (π β β!π β π΅ (π·β(πΉ β (π β πΊ))) < (π·βπΊ)) |