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