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={\mathrm{Poly}}_1\left(F\right)$$
	m1pmeq.m	$$⊢M={Monic}_{\mathrm{1p}}\left(F\right)$$
	m1pmeq.u	$$⊢U=\mathrm{Unit}\left(P\right)$$
	m1pmeq.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	m1pmeq.r	$$⊢\phi \to F\in \mathrm{Field}$$
	m1pmeq.f	$$⊢\phi \to I\in M$$
	m1pmeq.g	$$⊢\phi \to J\in M$$
	m1pmeq.h	$$⊢\phi \to K\in U$$
	m1pmeq.1	$$⊢\phi \to I=K\underset{\dot{}}{·}J$$
Assertion	m1pmeq	$$⊢\phi \to I=J$$

Proof

Step	Hyp	Ref	Expression
1		m1pmeq.p	$$⊢P={\mathrm{Poly}}_1\left(F\right)$$
2		m1pmeq.m	$$⊢M={Monic}_{\mathrm{1p}}\left(F\right)$$
3		m1pmeq.u	$$⊢U=\mathrm{Unit}\left(P\right)$$
4		m1pmeq.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
5		m1pmeq.r	$$⊢\phi \to F\in \mathrm{Field}$$
6		m1pmeq.f	$$⊢\phi \to I\in M$$
7		m1pmeq.g	$$⊢\phi \to J\in M$$
8		m1pmeq.h	$$⊢\phi \to K\in U$$
9		m1pmeq.1	$$⊢\phi \to I=K\underset{\dot{}}{·}J$$
10	5	flddrngd	$$⊢\phi \to F\in \mathrm{DivRing}$$
11	10	drngringd	$$⊢\phi \to F\in \mathrm{Ring}$$
12		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
13	12 3	unitcl	$$⊢K\in U\to K\in {\mathrm{Base}}_P$$
14	8 13	syl	$$⊢\phi \to K\in {\mathrm{Base}}_P$$
15	8 3	eleqtrdi	$$⊢\phi \to K\in \mathrm{Unit}\left(P\right)$$
16		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
17		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
18		eqid	$$⊢0_F=0_F$$
19		eqid	$$⊢{\mathrm{deg}}_1\left(F\right)={\mathrm{deg}}_1\left(F\right)$$
20	1 16 17 18 5 19 14	ply1unit	$$⊢\phi \to \left(K\in \mathrm{Unit}\left(P\right)\leftrightarrow {\mathrm{deg}}_1\left(F\right)\left(K\right)=0\right)$$
21	15 20	mpbid	$$⊢\phi \to {\mathrm{deg}}_1\left(F\right)\left(K\right)=0$$
22		0le0	$$⊢0\le 0$$
23	21 22	eqbrtrdi	$$⊢\phi \to {\mathrm{deg}}_1\left(F\right)\left(K\right)\le 0$$
24	19 1 12 16	deg1le0	$$⊢\left(F\in \mathrm{Ring}\wedge K\in {\mathrm{Base}}_P\right)\to \left({\mathrm{deg}}_1\left(F\right)\left(K\right)\le 0\leftrightarrow K=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(K\right)\left(0\right)\right)\right)$$
25	24	biimpa	$$⊢\left(\left(F\in \mathrm{Ring}\wedge K\in {\mathrm{Base}}_P\right)\wedge {\mathrm{deg}}_1\left(F\right)\left(K\right)\le 0\right)\to K=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(K\right)\left(0\right)\right)$$
26	11 14 23 25	syl21anc	$$⊢\phi \to K=\mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(K\right)\left(0\right)\right)$$
27		eqid	$$⊢{\cdot }_F={\cdot }_F$$
28		eqid	$$⊢1_F=1_F$$
29	21	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)={\mathrm{coe}}_1\left(K\right)\left(0\right)$$
30		0nn0	$$⊢0\in {\mathbb{N}}_0$$
31	21 30	eqeltrdi	$$⊢\phi \to {\mathrm{deg}}_1\left(F\right)\left(K\right)\in {\mathbb{N}}_0$$
32		eqid	$$⊢{\mathrm{coe}}_1\left(K\right)={\mathrm{coe}}_1\left(K\right)$$
33	32 12 1 17	coe1fvalcl	$$⊢\left(K\in {\mathrm{Base}}_P\wedge {\mathrm{deg}}_1\left(F\right)\left(K\right)\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\in {\mathrm{Base}}_F$$
34	14 31 33	syl2anc	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\in {\mathrm{Base}}_F$$
35	29 34	eqeltrrd	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left(0\right)\in {\mathrm{Base}}_F$$
36	17 27 28 11 35	ringridmd	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left(0\right){\cdot }_F{1}_F={\mathrm{coe}}_1\left(K\right)\left(0\right)$$
37	9	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(I\right)={\mathrm{coe}}_1\left(K\underset{\dot{}}{·}J\right)$$
38	9	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(F\right)\left(I\right)={\mathrm{deg}}_1\left(F\right)\left(K\underset{\dot{}}{·}J\right)$$
39		eqid	$$⊢\mathrm{RLReg}\left(F\right)=\mathrm{RLReg}\left(F\right)$$
40		eqid	$$⊢0_P=0_P$$
41		drngnzr	$$⊢F\in \mathrm{DivRing}\to F\in \mathrm{NzRing}$$
42	10 41	syl	$$⊢\phi \to F\in \mathrm{NzRing}$$
43	1	ply1nz	$$⊢F\in \mathrm{NzRing}\to P\in \mathrm{NzRing}$$
44	42 43	syl	$$⊢\phi \to P\in \mathrm{NzRing}$$
45	3 40 44 8	unitnz	$$⊢\phi \to K\ne 0_P$$
46		fldidom	$$⊢F\in \mathrm{Field}\to F\in \mathrm{IDomn}$$
47	5 46	syl	$$⊢\phi \to F\in \mathrm{IDomn}$$
48	47	idomdomd	$$⊢\phi \to F\in \mathrm{Domn}$$
49	19 1 18 12 40 11 14 23	deg1le0eq0	$$⊢\phi \to \left(K=0_P\leftrightarrow {\mathrm{coe}}_1\left(K\right)\left(0\right)=0_F\right)$$
50	49	necon3bid	$$⊢\phi \to \left(K\ne 0_P\leftrightarrow {\mathrm{coe}}_1\left(K\right)\left(0\right)\ne 0_F\right)$$
51	45 50	mpbid	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left(0\right)\ne 0_F$$
52	29 51	eqnetrd	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\ne 0_F$$
53	17 39 18	domnrrg	$$⊢\left(F\in \mathrm{Domn}\wedge {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\in {\mathrm{Base}}_F\wedge {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\ne 0_F\right)\to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\in \mathrm{RLReg}\left(F\right)$$
54	48 34 52 53	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right)\in \mathrm{RLReg}\left(F\right)$$
55	1 12 2	mon1pcl	$$⊢J\in M\to J\in {\mathrm{Base}}_P$$
56	7 55	syl	$$⊢\phi \to J\in {\mathrm{Base}}_P$$
57	1 40 2	mon1pn0	$$⊢J\in M\to J\ne 0_P$$
58	7 57	syl	$$⊢\phi \to J\ne 0_P$$
59	19 1 39 12 4 40 11 14 45 54 56 58	deg1mul2	$$⊢\phi \to {\mathrm{deg}}_1\left(F\right)\left(K\underset{\dot{}}{·}J\right)={\mathrm{deg}}_1\left(F\right)\left(K\right)+{\mathrm{deg}}_1\left(F\right)\left(J\right)$$
60	38 59	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(F\right)\left(I\right)={\mathrm{deg}}_1\left(F\right)\left(K\right)+{\mathrm{deg}}_1\left(F\right)\left(J\right)$$
61	37 60	fveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(I\right)\left({\mathrm{deg}}_1\left(F\right)\left(I\right)\right)={\mathrm{coe}}_1\left(K\underset{\dot{}}{·}J\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)+{\mathrm{deg}}_1\left(F\right)\left(J\right)\right)$$
62	19 28 2	mon1pldg	$$⊢I\in M\to {\mathrm{coe}}_1\left(I\right)\left({\mathrm{deg}}_1\left(F\right)\left(I\right)\right)=1_F$$
63	6 62	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(I\right)\left({\mathrm{deg}}_1\left(F\right)\left(I\right)\right)=1_F$$
64	1 4 27 12 19 40 11 14 45 56 58	coe1mul4	$$⊢\phi \to {\mathrm{coe}}_1\left(K\underset{\dot{}}{·}J\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)+{\mathrm{deg}}_1\left(F\right)\left(J\right)\right)={\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right){\cdot }_F{\mathrm{coe}}_1\left(J\right)\left({\mathrm{deg}}_1\left(F\right)\left(J\right)\right)$$
65	19 28 2	mon1pldg	$$⊢J\in M\to {\mathrm{coe}}_1\left(J\right)\left({\mathrm{deg}}_1\left(F\right)\left(J\right)\right)=1_F$$
66	7 65	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(J\right)\left({\mathrm{deg}}_1\left(F\right)\left(J\right)\right)=1_F$$
67	29 66	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)\right){\cdot }_F{\mathrm{coe}}_1\left(J\right)\left({\mathrm{deg}}_1\left(F\right)\left(J\right)\right)={\mathrm{coe}}_1\left(K\right)\left(0\right){\cdot }_F{1}_F$$
68	64 67	eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(K\underset{\dot{}}{·}J\right)\left({\mathrm{deg}}_1\left(F\right)\left(K\right)+{\mathrm{deg}}_1\left(F\right)\left(J\right)\right)={\mathrm{coe}}_1\left(K\right)\left(0\right){\cdot }_F{1}_F$$
69	61 63 68	3eqtr3rd	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left(0\right){\cdot }_F{1}_F=1_F$$
70	36 69	eqtr3d	$$⊢\phi \to {\mathrm{coe}}_1\left(K\right)\left(0\right)=1_F$$
71	70	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left({\mathrm{coe}}_1\left(K\right)\left(0\right)\right)=\mathrm{algSc}\left(P\right)\left(1_F\right)$$
72		eqid	$$⊢1_P=1_P$$
73	1 16 28 72 11	ply1ascl1	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(1_F\right)=1_P$$
74	26 71 73	3eqtrd	$$⊢\phi \to K=1_P$$
75	74	oveq1d	$$⊢\phi \to K\underset{\dot{}}{·}J=1_P\underset{\dot{}}{·}J$$
76	1	ply1ring	$$⊢F\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
77	11 76	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
78	12 4 72 77 56	ringlidmd	$$⊢\phi \to 1_P\underset{\dot{}}{·}J=J$$
79	9 75 78	3eqtrd	$$⊢\phi \to I=J$$