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 ⊢ 𝑃 = ( Poly1 ‘ 𝐹 )
m1pmeq.m ⊢ 𝑀 = ( Monic1p ‘ 𝐹 )
m1pmeq.u ⊢ 𝑈 = ( Unit ‘ 𝑃 )
m1pmeq.t ⊢ · = ( .r ‘ 𝑃 )
m1pmeq.r ⊢ ( 𝜑 → 𝐹 ∈ Field )
m1pmeq.f ⊢ ( 𝜑 → 𝐼 ∈ 𝑀 )
m1pmeq.g ⊢ ( 𝜑 → 𝐽 ∈ 𝑀 )
m1pmeq.h ⊢ ( 𝜑 → 𝐾 ∈ 𝑈 )
m1pmeq.1 ⊢ ( 𝜑 → 𝐼 = ( 𝐾 · 𝐽 ) )
Assertion m1pmeq ( 𝜑 → 𝐼 = 𝐽 )

Proof

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