Step |
Hyp |
Ref |
Expression |
1 |
|
ply1divalg.p |
|- P = ( Poly1 ` R ) |
2 |
|
ply1divalg.d |
|- D = ( deg1 ` R ) |
3 |
|
ply1divalg.b |
|- B = ( Base ` P ) |
4 |
|
ply1divalg.m |
|- .- = ( -g ` P ) |
5 |
|
ply1divalg.z |
|- .0. = ( 0g ` P ) |
6 |
|
ply1divalg.t |
|- .xb = ( .r ` P ) |
7 |
|
ply1divalg.r1 |
|- ( ph -> R e. Ring ) |
8 |
|
ply1divalg.f |
|- ( ph -> F e. B ) |
9 |
|
ply1divalg.g1 |
|- ( ph -> G e. B ) |
10 |
|
ply1divalg.g2 |
|- ( ph -> G =/= .0. ) |
11 |
|
ply1divalg.g3 |
|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. U ) |
12 |
|
ply1divalg.u |
|- U = ( Unit ` R ) |
13 |
|
eqid |
|- ( Poly1 ` ( oppR ` R ) ) = ( Poly1 ` ( oppR ` R ) ) |
14 |
|
eqidd |
|- ( T. -> ( Base ` R ) = ( Base ` R ) ) |
15 |
|
eqid |
|- ( oppR ` R ) = ( oppR ` R ) |
16 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
17 |
15 16
|
opprbas |
|- ( Base ` R ) = ( Base ` ( oppR ` R ) ) |
18 |
17
|
a1i |
|- ( T. -> ( Base ` R ) = ( Base ` ( oppR ` R ) ) ) |
19 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
20 |
15 19
|
oppradd |
|- ( +g ` R ) = ( +g ` ( oppR ` R ) ) |
21 |
20
|
oveqi |
|- ( q ( +g ` R ) r ) = ( q ( +g ` ( oppR ` R ) ) r ) |
22 |
21
|
a1i |
|- ( ( T. /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( +g ` R ) r ) = ( q ( +g ` ( oppR ` R ) ) r ) ) |
23 |
14 18 22
|
deg1propd |
|- ( T. -> ( deg1 ` R ) = ( deg1 ` ( oppR ` R ) ) ) |
24 |
23
|
mptru |
|- ( deg1 ` R ) = ( deg1 ` ( oppR ` R ) ) |
25 |
2 24
|
eqtri |
|- D = ( deg1 ` ( oppR ` R ) ) |
26 |
1
|
fveq2i |
|- ( Base ` P ) = ( Base ` ( Poly1 ` R ) ) |
27 |
14 18 22
|
ply1baspropd |
|- ( T. -> ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` ( oppR ` R ) ) ) ) |
28 |
27
|
mptru |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` ( oppR ` R ) ) ) |
29 |
26 28
|
eqtri |
|- ( Base ` P ) = ( Base ` ( Poly1 ` ( oppR ` R ) ) ) |
30 |
3 29
|
eqtri |
|- B = ( Base ` ( Poly1 ` ( oppR ` R ) ) ) |
31 |
29
|
a1i |
|- ( T. -> ( Base ` P ) = ( Base ` ( Poly1 ` ( oppR ` R ) ) ) ) |
32 |
1
|
fveq2i |
|- ( +g ` P ) = ( +g ` ( Poly1 ` R ) ) |
33 |
14 18 22
|
ply1plusgpropd |
|- ( T. -> ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` ( oppR ` R ) ) ) ) |
34 |
33
|
mptru |
|- ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` ( oppR ` R ) ) ) |
35 |
32 34
|
eqtri |
|- ( +g ` P ) = ( +g ` ( Poly1 ` ( oppR ` R ) ) ) |
36 |
35
|
a1i |
|- ( T. -> ( +g ` P ) = ( +g ` ( Poly1 ` ( oppR ` R ) ) ) ) |
37 |
31 36
|
grpsubpropd |
|- ( T. -> ( -g ` P ) = ( -g ` ( Poly1 ` ( oppR ` R ) ) ) ) |
38 |
37
|
mptru |
|- ( -g ` P ) = ( -g ` ( Poly1 ` ( oppR ` R ) ) ) |
39 |
4 38
|
eqtri |
|- .- = ( -g ` ( Poly1 ` ( oppR ` R ) ) ) |
40 |
3
|
a1i |
|- ( T. -> B = ( Base ` P ) ) |
41 |
30
|
a1i |
|- ( T. -> B = ( Base ` ( Poly1 ` ( oppR ` R ) ) ) ) |
42 |
35
|
oveqi |
|- ( q ( +g ` P ) r ) = ( q ( +g ` ( Poly1 ` ( oppR ` R ) ) ) r ) |
43 |
42
|
a1i |
|- ( ( T. /\ ( q e. B /\ r e. B ) ) -> ( q ( +g ` P ) r ) = ( q ( +g ` ( Poly1 ` ( oppR ` R ) ) ) r ) ) |
44 |
40 41 43
|
grpidpropd |
|- ( T. -> ( 0g ` P ) = ( 0g ` ( Poly1 ` ( oppR ` R ) ) ) ) |
45 |
44
|
mptru |
|- ( 0g ` P ) = ( 0g ` ( Poly1 ` ( oppR ` R ) ) ) |
46 |
5 45
|
eqtri |
|- .0. = ( 0g ` ( Poly1 ` ( oppR ` R ) ) ) |
47 |
|
eqid |
|- ( .r ` ( Poly1 ` ( oppR ` R ) ) ) = ( .r ` ( Poly1 ` ( oppR ` R ) ) ) |
48 |
15
|
opprring |
|- ( R e. Ring -> ( oppR ` R ) e. Ring ) |
49 |
7 48
|
syl |
|- ( ph -> ( oppR ` R ) e. Ring ) |
50 |
12 15
|
opprunit |
|- U = ( Unit ` ( oppR ` R ) ) |
51 |
13 25 30 39 46 47 49 8 9 10 11 50
|
ply1divalg |
|- ( ph -> E! q e. B ( D ` ( F .- ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) ) ) < ( D ` G ) ) |
52 |
7
|
adantr |
|- ( ( ph /\ q e. B ) -> R e. Ring ) |
53 |
9
|
adantr |
|- ( ( ph /\ q e. B ) -> G e. B ) |
54 |
|
simpr |
|- ( ( ph /\ q e. B ) -> q e. B ) |
55 |
1 15 13 6 47 3
|
ply1opprmul |
|- ( ( R e. Ring /\ G e. B /\ q e. B ) -> ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) = ( q .xb G ) ) |
56 |
52 53 54 55
|
syl3anc |
|- ( ( ph /\ q e. B ) -> ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) = ( q .xb G ) ) |
57 |
56
|
eqcomd |
|- ( ( ph /\ q e. B ) -> ( q .xb G ) = ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) ) |
58 |
57
|
oveq2d |
|- ( ( ph /\ q e. B ) -> ( F .- ( q .xb G ) ) = ( F .- ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) ) ) |
59 |
58
|
fveq2d |
|- ( ( ph /\ q e. B ) -> ( D ` ( F .- ( q .xb G ) ) ) = ( D ` ( F .- ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) ) ) ) |
60 |
59
|
breq1d |
|- ( ( ph /\ q e. B ) -> ( ( D ` ( F .- ( q .xb G ) ) ) < ( D ` G ) <-> ( D ` ( F .- ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) ) ) < ( D ` G ) ) ) |
61 |
60
|
reubidva |
|- ( ph -> ( E! q e. B ( D ` ( F .- ( q .xb G ) ) ) < ( D ` G ) <-> E! q e. B ( D ` ( F .- ( G ( .r ` ( Poly1 ` ( oppR ` R ) ) ) q ) ) ) < ( D ` G ) ) ) |
62 |
51 61
|
mpbird |
|- ( ph -> E! q e. B ( D ` ( F .- ( q .xb G ) ) ) < ( D ` G ) ) |