Metamath Proof Explorer

Theorem m1pmeq

Description: If two monic polynomials I and J differ by a unit factor K , then they are equal. (Contributed by Thierry Arnoux, 27-Apr-2025)

Ref Expression
Hypotheses m1pmeq.p 
|- P = ( Poly1 ` F )
m1pmeq.m 
|- M = ( Monic1p ` F )
m1pmeq.u 
|- U = ( Unit ` P )
m1pmeq.t 
|- .x. = ( .r ` P )
m1pmeq.r 
|- ( ph -> F e. Field )
m1pmeq.f 
|- ( ph -> I e. M )
m1pmeq.g 
|- ( ph -> J e. M )
m1pmeq.h 
|- ( ph -> K e. U )
m1pmeq.1 
|- ( ph -> I = ( K .x. J ) )
Assertion m1pmeq 
|- ( ph -> I = J )

Proof

Step Hyp Ref Expression
1 m1pmeq.p 
 |-  P = ( Poly1 ` F )
2 m1pmeq.m 
 |-  M = ( Monic1p ` F )
3 m1pmeq.u 
 |-  U = ( Unit ` P )
4 m1pmeq.t 
 |-  .x. = ( .r ` P )
5 m1pmeq.r 
 |-  ( ph -> F e. Field )
6 m1pmeq.f 
 |-  ( ph -> I e. M )
7 m1pmeq.g 
 |-  ( ph -> J e. M )
8 m1pmeq.h 
 |-  ( ph -> K e. U )
9 m1pmeq.1 
 |-  ( ph -> I = ( K .x. J ) )
10 5 flddrngd 
 |-  ( ph -> F e. DivRing )
11 10 drngringd 
 |-  ( ph -> F e. Ring )
12 eqid 
 |-  ( Base ` P ) = ( Base ` P )
13 12 3 unitcl 
 |-  ( K e. U -> K e. ( Base ` P ) )
14 8 13 syl 
 |-  ( ph -> K e. ( Base ` P ) )
15 8 3 eleqtrdi 
 |-  ( ph -> K e. ( Unit ` P ) )
16 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
17 eqid 
 |-  ( Base ` F ) = ( Base ` F )
18 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
19 eqid 
 |-  ( deg1 ` F ) = ( deg1 ` F )
20 1 16 17 18 5 19 14 ply1unit 
 |-  ( ph -> ( K e. ( Unit ` P ) <-> ( ( deg1 ` F ) ` K ) = 0 ) )
21 15 20 mpbid 
 |-  ( ph -> ( ( deg1 ` F ) ` K ) = 0 )
22 0le0 
 |-  0 <_ 0
23 21 22 eqbrtrdi 
 |-  ( ph -> ( ( deg1 ` F ) ` K ) <_ 0 )
24 19 1 12 16 deg1le0 
 |-  ( ( F e. Ring /\ K e. ( Base ` P ) ) -> ( ( ( deg1 ` F ) ` K ) <_ 0 <-> K = ( ( algSc ` P ) ` ( ( coe1 ` K ) ` 0 ) ) ) )
25 24 biimpa 
 |-  ( ( ( F e. Ring /\ K e. ( Base ` P ) ) /\ ( ( deg1 ` F ) ` K ) <_ 0 ) -> K = ( ( algSc ` P ) ` ( ( coe1 ` K ) ` 0 ) ) )
26 11 14 23 25 syl21anc 
 |-  ( ph -> K = ( ( algSc ` P ) ` ( ( coe1 ` K ) ` 0 ) ) )
27 eqid 
 |-  ( .r ` F ) = ( .r ` F )
28 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
29 21 fveq2d 
 |-  ( ph -> ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) = ( ( coe1 ` K ) ` 0 ) )
30 0nn0 
 |-  0 e. NN0
31 21 30 eqeltrdi 
 |-  ( ph -> ( ( deg1 ` F ) ` K ) e. NN0 )
32 eqid 
 |-  ( coe1 ` K ) = ( coe1 ` K )
33 32 12 1 17 coe1fvalcl 
 |-  ( ( K e. ( Base ` P ) /\ ( ( deg1 ` F ) ` K ) e. NN0 ) -> ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) e. ( Base ` F ) )
34 14 31 33 syl2anc 
 |-  ( ph -> ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) e. ( Base ` F ) )
35 29 34 eqeltrrd 
 |-  ( ph -> ( ( coe1 ` K ) ` 0 ) e. ( Base ` F ) )
36 17 27 28 11 35 ringridmd 
 |-  ( ph -> ( ( ( coe1 ` K ) ` 0 ) ( .r ` F ) ( 1r ` F ) ) = ( ( coe1 ` K ) ` 0 ) )
37 9 fveq2d 
 |-  ( ph -> ( coe1 ` I ) = ( coe1 ` ( K .x. J ) ) )
38 9 fveq2d 
 |-  ( ph -> ( ( deg1 ` F ) ` I ) = ( ( deg1 ` F ) ` ( K .x. J ) ) )
39 eqid 
 |-  ( RLReg ` F ) = ( RLReg ` F )
40 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
41 drngnzr 
 |-  ( F e. DivRing -> F e. NzRing )
42 10 41 syl 
 |-  ( ph -> F e. NzRing )
43 1 ply1nz 
 |-  ( F e. NzRing -> P e. NzRing )
44 42 43 syl 
 |-  ( ph -> P e. NzRing )
45 3 40 44 8 unitnz 
 |-  ( ph -> K =/= ( 0g ` P ) )
46 fldidom 
 |-  ( F e. Field -> F e. IDomn )
47 5 46 syl 
 |-  ( ph -> F e. IDomn )
48 47 idomdomd 
 |-  ( ph -> F e. Domn )
49 19 1 18 12 40 11 14 23 deg1le0eq0 
 |-  ( ph -> ( K = ( 0g ` P ) <-> ( ( coe1 ` K ) ` 0 ) = ( 0g ` F ) ) )
50 49 necon3bid 
 |-  ( ph -> ( K =/= ( 0g ` P ) <-> ( ( coe1 ` K ) ` 0 ) =/= ( 0g ` F ) ) )
51 45 50 mpbid 
 |-  ( ph -> ( ( coe1 ` K ) ` 0 ) =/= ( 0g ` F ) )
52 29 51 eqnetrd 
 |-  ( ph -> ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) =/= ( 0g ` F ) )
53 17 39 18 domnrrg 
 |-  ( ( F e. Domn /\ ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) e. ( Base ` F ) /\ ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) =/= ( 0g ` F ) ) -> ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) e. ( RLReg ` F ) )
54 48 34 52 53 syl3anc 
 |-  ( ph -> ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) e. ( RLReg ` F ) )
55 1 12 2 mon1pcl 
 |-  ( J e. M -> J e. ( Base ` P ) )
56 7 55 syl 
 |-  ( ph -> J e. ( Base ` P ) )
57 1 40 2 mon1pn0 
 |-  ( J e. M -> J =/= ( 0g ` P ) )
58 7 57 syl 
 |-  ( ph -> J =/= ( 0g ` P ) )
59 19 1 39 12 4 40 11 14 45 54 56 58 deg1mul2 
 |-  ( ph -> ( ( deg1 ` F ) ` ( K .x. J ) ) = ( ( ( deg1 ` F ) ` K ) + ( ( deg1 ` F ) ` J ) ) )
60 38 59 eqtrd 
 |-  ( ph -> ( ( deg1 ` F ) ` I ) = ( ( ( deg1 ` F ) ` K ) + ( ( deg1 ` F ) ` J ) ) )
61 37 60 fveq12d 
 |-  ( ph -> ( ( coe1 ` I ) ` ( ( deg1 ` F ) ` I ) ) = ( ( coe1 ` ( K .x. J ) ) ` ( ( ( deg1 ` F ) ` K ) + ( ( deg1 ` F ) ` J ) ) ) )
62 19 28 2 mon1pldg 
 |-  ( I e. M -> ( ( coe1 ` I ) ` ( ( deg1 ` F ) ` I ) ) = ( 1r ` F ) )
63 6 62 syl 
 |-  ( ph -> ( ( coe1 ` I ) ` ( ( deg1 ` F ) ` I ) ) = ( 1r ` F ) )
64 1 4 27 12 19 40 11 14 45 56 58 coe1mul4 
 |-  ( ph -> ( ( coe1 ` ( K .x. J ) ) ` ( ( ( deg1 ` F ) ` K ) + ( ( deg1 ` F ) ` J ) ) ) = ( ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) ( .r ` F ) ( ( coe1 ` J ) ` ( ( deg1 ` F ) ` J ) ) ) )
65 19 28 2 mon1pldg 
 |-  ( J e. M -> ( ( coe1 ` J ) ` ( ( deg1 ` F ) ` J ) ) = ( 1r ` F ) )
66 7 65 syl 
 |-  ( ph -> ( ( coe1 ` J ) ` ( ( deg1 ` F ) ` J ) ) = ( 1r ` F ) )
67 29 66 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` K ) ` ( ( deg1 ` F ) ` K ) ) ( .r ` F ) ( ( coe1 ` J ) ` ( ( deg1 ` F ) ` J ) ) ) = ( ( ( coe1 ` K ) ` 0 ) ( .r ` F ) ( 1r ` F ) ) )
68 64 67 eqtrd 
 |-  ( ph -> ( ( coe1 ` ( K .x. J ) ) ` ( ( ( deg1 ` F ) ` K ) + ( ( deg1 ` F ) ` J ) ) ) = ( ( ( coe1 ` K ) ` 0 ) ( .r ` F ) ( 1r ` F ) ) )
69 61 63 68 3eqtr3rd 
 |-  ( ph -> ( ( ( coe1 ` K ) ` 0 ) ( .r ` F ) ( 1r ` F ) ) = ( 1r ` F ) )
70 36 69 eqtr3d 
 |-  ( ph -> ( ( coe1 ` K ) ` 0 ) = ( 1r ` F ) )
71 70 fveq2d 
 |-  ( ph -> ( ( algSc ` P ) ` ( ( coe1 ` K ) ` 0 ) ) = ( ( algSc ` P ) ` ( 1r ` F ) ) )
72 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
73 1 16 28 72 11 ply1ascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` F ) ) = ( 1r ` P ) )
74 26 71 73 3eqtrd 
 |-  ( ph -> K = ( 1r ` P ) )
75 74 oveq1d 
 |-  ( ph -> ( K .x. J ) = ( ( 1r ` P ) .x. J ) )
76 1 ply1ring 
 |-  ( F e. Ring -> P e. Ring )
77 11 76 syl 
 |-  ( ph -> P e. Ring )
78 12 4 72 77 56 ringlidmd 
 |-  ( ph -> ( ( 1r ` P ) .x. J ) = J )
79 9 75 78 3eqtrd 
 |-  ( ph -> I = J )