Metamath Proof Explorer

Theorem ply1divalg3

Description: Uniqueness of polynomial remainder: convert the subtraction in ply1divalg2 to addition. (Contributed by SN, 20-Jun-2025)

Ref Expression
Hypotheses ply1divalg3.p 
|- P = ( Poly1 ` R )
ply1divalg3.d 
|- D = ( deg1 ` R )
ply1divalg3.b 
|- B = ( Base ` P )
ply1divalg3.m 
|- .+ = ( +g ` P )
ply1divalg3.t 
|- .xb = ( .r ` P )
ply1divalg3.c 
|- C = ( Unic1p ` R )
ply1divalg3.r 
|- ( ph -> R e. Ring )
ply1divalg3.f 
|- ( ph -> F e. B )
ply1divalg3.g 
|- ( ph -> G e. C )
Assertion ply1divalg3 
|- ( ph -> E! q e. B ( D ` ( F .+ ( q .xb G ) ) ) < ( D ` G ) )

Proof

Step Hyp Ref Expression
1 ply1divalg3.p 
 |-  P = ( Poly1 ` R )
2 ply1divalg3.d 
 |-  D = ( deg1 ` R )
3 ply1divalg3.b 
 |-  B = ( Base ` P )
4 ply1divalg3.m 
 |-  .+ = ( +g ` P )
5 ply1divalg3.t 
 |-  .xb = ( .r ` P )
6 ply1divalg3.c 
 |-  C = ( Unic1p ` R )
7 ply1divalg3.r 
 |-  ( ph -> R e. Ring )
8 ply1divalg3.f 
 |-  ( ph -> F e. B )
9 ply1divalg3.g 
 |-  ( ph -> G e. C )
10 eqid 
 |-  ( -g ` P ) = ( -g ` P )
11 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
12 1 3 6 uc1pcl 
 |-  ( G e. C -> G e. B )
13 9 12 syl 
 |-  ( ph -> G e. B )
14 1 11 6 uc1pn0 
 |-  ( G e. C -> G =/= ( 0g ` P ) )
15 9 14 syl 
 |-  ( ph -> G =/= ( 0g ` P ) )
16 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
17 2 16 6 uc1pldg 
 |-  ( G e. C -> ( ( coe1 ` G ) ` ( D ` G ) ) e. ( Unit ` R ) )
18 9 17 syl 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. ( Unit ` R ) )
19 1 2 3 10 11 5 7 8 13 15 18 16 ply1divalg2 
 |-  ( ph -> E! p e. B ( D ` ( F ( -g ` P ) ( p .xb G ) ) ) < ( D ` G ) )
20 eqid 
 |-  ( invg ` P ) = ( invg ` P )
21 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
22 7 21 syl 
 |-  ( ph -> P e. Ring )
23 22 ringgrpd 
 |-  ( ph -> P e. Grp )
24 23 adantr 
 |-  ( ( ph /\ q e. B ) -> P e. Grp )
25 simpr 
 |-  ( ( ph /\ q e. B ) -> q e. B )
26 3 20 24 25 grpinvcld 
 |-  ( ( ph /\ q e. B ) -> ( ( invg ` P ) ` q ) e. B )
27 3 20 23 grpinvf1o 
 |-  ( ph -> ( invg ` P ) : B -1-1-onto-> B )
28 f1ofveu 
 |-  ( ( ( invg ` P ) : B -1-1-onto-> B /\ p e. B ) -> E! q e. B ( ( invg ` P ) ` q ) = p )
29 27 28 sylan 
 |-  ( ( ph /\ p e. B ) -> E! q e. B ( ( invg ` P ) ` q ) = p )
30 eqcom 
 |-  ( p = ( ( invg ` P ) ` q ) <-> ( ( invg ` P ) ` q ) = p )
31 30 reubii 
 |-  ( E! q e. B p = ( ( invg ` P ) ` q ) <-> E! q e. B ( ( invg ` P ) ` q ) = p )
32 29 31 sylibr 
 |-  ( ( ph /\ p e. B ) -> E! q e. B p = ( ( invg ` P ) ` q ) )
33 oveq1 
 |-  ( p = ( ( invg ` P ) ` q ) -> ( p .xb G ) = ( ( ( invg ` P ) ` q ) .xb G ) )
34 33 oveq2d 
 |-  ( p = ( ( invg ` P ) ` q ) -> ( F ( -g ` P ) ( p .xb G ) ) = ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) )
35 34 fveq2d 
 |-  ( p = ( ( invg ` P ) ` q ) -> ( D ` ( F ( -g ` P ) ( p .xb G ) ) ) = ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) )
36 35 breq1d 
 |-  ( p = ( ( invg ` P ) ` q ) -> ( ( D ` ( F ( -g ` P ) ( p .xb G ) ) ) < ( D ` G ) <-> ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) < ( D ` G ) ) )
37 26 32 36 reuxfr1ds 
 |-  ( ph -> ( E! p e. B ( D ` ( F ( -g ` P ) ( p .xb G ) ) ) < ( D ` G ) <-> E! q e. B ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) < ( D ` G ) ) )
38 19 37 mpbid 
 |-  ( ph -> E! q e. B ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) < ( D ` G ) )
39 22 adantr 
 |-  ( ( ph /\ q e. B ) -> P e. Ring )
40 13 adantr 
 |-  ( ( ph /\ q e. B ) -> G e. B )
41 3 5 39 26 40 ringcld 
 |-  ( ( ph /\ q e. B ) -> ( ( ( invg ` P ) ` q ) .xb G ) e. B )
42 3 4 20 10 grpsubval 
 |-  ( ( F e. B /\ ( ( ( invg ` P ) ` q ) .xb G ) e. B ) -> ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) = ( F .+ ( ( invg ` P ) ` ( ( ( invg ` P ) ` q ) .xb G ) ) ) )
43 8 41 42 syl2an2r 
 |-  ( ( ph /\ q e. B ) -> ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) = ( F .+ ( ( invg ` P ) ` ( ( ( invg ` P ) ` q ) .xb G ) ) ) )
44 3 5 20 39 25 40 ringmneg1 
 |-  ( ( ph /\ q e. B ) -> ( ( ( invg ` P ) ` q ) .xb G ) = ( ( invg ` P ) ` ( q .xb G ) ) )
45 44 fveq2d 
 |-  ( ( ph /\ q e. B ) -> ( ( invg ` P ) ` ( ( ( invg ` P ) ` q ) .xb G ) ) = ( ( invg ` P ) ` ( ( invg ` P ) ` ( q .xb G ) ) ) )
46 3 5 39 25 40 ringcld 
 |-  ( ( ph /\ q e. B ) -> ( q .xb G ) e. B )
47 3 20 grpinvinv 
 |-  ( ( P e. Grp /\ ( q .xb G ) e. B ) -> ( ( invg ` P ) ` ( ( invg ` P ) ` ( q .xb G ) ) ) = ( q .xb G ) )
48 23 46 47 syl2an2r 
 |-  ( ( ph /\ q e. B ) -> ( ( invg ` P ) ` ( ( invg ` P ) ` ( q .xb G ) ) ) = ( q .xb G ) )
49 45 48 eqtrd 
 |-  ( ( ph /\ q e. B ) -> ( ( invg ` P ) ` ( ( ( invg ` P ) ` q ) .xb G ) ) = ( q .xb G ) )
50 49 oveq2d 
 |-  ( ( ph /\ q e. B ) -> ( F .+ ( ( invg ` P ) ` ( ( ( invg ` P ) ` q ) .xb G ) ) ) = ( F .+ ( q .xb G ) ) )
51 43 50 eqtrd 
 |-  ( ( ph /\ q e. B ) -> ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) = ( F .+ ( q .xb G ) ) )
52 51 fveq2d 
 |-  ( ( ph /\ q e. B ) -> ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) = ( D ` ( F .+ ( q .xb G ) ) ) )
53 52 breq1d 
 |-  ( ( ph /\ q e. B ) -> ( ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) < ( D ` G ) <-> ( D ` ( F .+ ( q .xb G ) ) ) < ( D ` G ) ) )
54 53 reubidva 
 |-  ( ph -> ( E! q e. B ( D ` ( F ( -g ` P ) ( ( ( invg ` P ) ` q ) .xb G ) ) ) < ( D ` G ) <-> E! q e. B ( D ` ( F .+ ( q .xb G ) ) ) < ( D ` G ) ) )
55 38 54 mpbid 
 |-  ( ph -> E! q e. B ( D ` ( F .+ ( q .xb G ) ) ) < ( D ` G ) )