Metamath Proof Explorer


Theorem ply1divalg2

Description: Reverse the order of multiplication in ply1divalg via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1divalg.p
|- P = ( Poly1 ` R )
ply1divalg.d
|- D = ( deg1 ` R )
ply1divalg.b
|- B = ( Base ` P )
ply1divalg.m
|- .- = ( -g ` P )
ply1divalg.z
|- .0. = ( 0g ` P )
ply1divalg.t
|- .xb = ( .r ` P )
ply1divalg.r1
|- ( ph -> R e. Ring )
ply1divalg.f
|- ( ph -> F e. B )
ply1divalg.g1
|- ( ph -> G e. B )
ply1divalg.g2
|- ( ph -> G =/= .0. )
ply1divalg.g3
|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. U )
ply1divalg.u
|- U = ( Unit ` R )
Assertion ply1divalg2
|- ( ph -> E! q e. B ( D ` ( F .- ( q .xb G ) ) ) < ( D ` G ) )

Proof

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 ) )