ply1edom

Description: The univariate polynomials over a field R form a Euclidean domain. Note that the hypothesis ( deg1R ) = ( EuclFP ) could be dropped if the definition of Poly1 would be adapted. (Contributed by Thierry Arnoux, 9-Nov-2026)

	Ref	Expression
Hypotheses	ply1edom.1	$⊢ P = {Poly}_{1} (R)$
	ply1edom.2	$⊢ U = {Base}_{P}$
	ply1edom.3	$⊢ Z = 0_{P}$
	ply1edom.4	$⊢ \deg_{1} (R) = EuclF (P)$
	ply1edom.5	$⊢ φ \to R \in Field$
Assertion	ply1edom	$⊢ φ \to P \in EDomn$

Proof

Step	Hyp	Ref	Expression
1		ply1edom.1	$⊢ P = {Poly}_{1} (R)$
2		ply1edom.2	$⊢ U = {Base}_{P}$
3		ply1edom.3	$⊢ Z = 0_{P}$
4		ply1edom.4	$⊢ \deg_{1} (R) = EuclF (P)$
5		ply1edom.5	$⊢ φ \to R \in Field$
6		fldidom	$⊢ R \in Field \to R \in IDomn$
7	5 6	syl	$⊢ φ \to R \in IDomn$
8	1	ply1idom	$⊢ R \in IDomn \to P \in IDomn$
9	7 8	syl	$⊢ φ \to P \in IDomn$
10		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
11	10 1 2	deg1xrf	$⊢ \deg_{1} (R) : U ⟶ ℝ^{*}$
12	11	a1i	$⊢ φ \to \deg_{1} (R) : U ⟶ ℝ^{*}$
13		difssd	$⊢ φ \to U ∖ \{Z\} \subseteq U$
14		nfv	$⊢ Ⅎ f φ$
15	12	ffund	$⊢ φ \to Fun \deg_{1} (R)$
16	7	idomringd	$⊢ φ \to R \in Ring$
17	16	adantr	$⊢ (φ \land f \in (U ∖ \{Z\})) \to R \in Ring$
18	13	sselda	$⊢ (φ \land f \in (U ∖ \{Z\})) \to f \in U$
19		simpr	$⊢ (φ \land f \in (U ∖ \{Z\})) \to f \in (U ∖ \{Z\})$
20	19	eldifsnbd	$⊢ (φ \land f \in (U ∖ \{Z\})) \to f \neq Z$
21	10 1 3 2	deg1nn0cl	$⊢ (R \in Ring \land f \in U \land f \neq Z) \to \deg_{1} (R) (f) \in ℕ_{0}$
22	17 18 20 21	syl3anc	$⊢ (φ \land f \in (U ∖ \{Z\})) \to \deg_{1} (R) (f) \in ℕ_{0}$
23	14 15 22	funimassd	$⊢ φ \to \deg_{1} (R) [U ∖ \{Z\}] \subseteq ℕ_{0}$
24	12 13 23	fssrescdmd	$⊢ φ \to ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) : U ∖ \{Z\} ⟶ ℕ_{0}$
25		oveq2	$⊢ q = f {quot}_{1p} (R) g \to g \cdot_{P} q = g \cdot_{P} (f {quot}_{1p} (R) g)$
26	25	oveq1d	$⊢ q = f {quot}_{1p} (R) g \to (g \cdot_{P} q) +_{P} r = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} r$
27	26	eqeq2d	$⊢ q = f {quot}_{1p} (R) g \to (f = (g \cdot_{P} q) +_{P} r \leftrightarrow f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} r)$
28	27	anbi1d	$⊢ q = f {quot}_{1p} (R) g \to ((f = (g \cdot_{P} q) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))) \leftrightarrow (f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))))$
29		oveq2	$⊢ r = f {rem}_{1p} (R) g \to (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} r = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} (f {rem}_{1p} (R) g)$
30	29	eqeq2d	$⊢ r = f {rem}_{1p} (R) g \to (f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} r \leftrightarrow f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} (f {rem}_{1p} (R) g))$
31		eqeq1	$⊢ r = f {rem}_{1p} (R) g \to (r = Z \leftrightarrow f {rem}_{1p} (R) g = Z)$
32		fveq2	$⊢ r = f {rem}_{1p} (R) g \to ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) = ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g)$
33	32	breq1d	$⊢ r = f {rem}_{1p} (R) g \to (({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g) \leftrightarrow ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))$
34	31 33	orbi12d	$⊢ r = f {rem}_{1p} (R) g \to ((r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)) \leftrightarrow (f {rem}_{1p} (R) g = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)))$
35	30 34	anbi12d	$⊢ r = f {rem}_{1p} (R) g \to ((f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))) \leftrightarrow (f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} (f {rem}_{1p} (R) g) \land (f {rem}_{1p} (R) g = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))))$
36	16	ad2antrr	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to R \in Ring$
37		simplr	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to f \in U$
38	5	flddrngd	$⊢ φ \to R \in DivRing$
39	38	ad2antrr	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to R \in DivRing$
40		simpr	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to g \in (U ∖ \{Z\})$
41	40	eldifad	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to g \in U$
42	40	eldifsnbd	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to g \neq Z$
43		eqid	$⊢ {Unic}_{1p} (R) = {Unic}_{1p} (R)$
44	1 2 3 43	drnguc1p	$⊢ (R \in DivRing \land g \in U \land g \neq Z) \to g \in {Unic}_{1p} (R)$
45	39 41 42 44	syl3anc	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to g \in {Unic}_{1p} (R)$
46		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
47	46 1 2 43	q1pcl	$⊢ (R \in Ring \land f \in U \land g \in {Unic}_{1p} (R)) \to f {quot}_{1p} (R) g \in U$
48	36 37 45 47	syl3anc	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to f {quot}_{1p} (R) g \in U$
49		eqid	$⊢ {rem}_{1p} (R) = {rem}_{1p} (R)$
50	49 1 2 43	r1pcl	$⊢ (R \in Ring \land f \in U \land g \in {Unic}_{1p} (R)) \to f {rem}_{1p} (R) g \in U$
51	36 37 45 50	syl3anc	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to f {rem}_{1p} (R) g \in U$
52		eqid	$⊢ \cdot_{P} = \cdot_{P}$
53		eqid	$⊢ +_{P} = +_{P}$
54	1 2 43 46 49 52 53	r1pid	$⊢ (R \in Ring \land f \in U \land g \in {Unic}_{1p} (R)) \to f = ((f {quot}_{1p} (R) g) \cdot_{P} g) +_{P} (f {rem}_{1p} (R) g)$
55	36 37 45 54	syl3anc	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to f = ((f {quot}_{1p} (R) g) \cdot_{P} g) +_{P} (f {rem}_{1p} (R) g)$
56	9	idomcringd	$⊢ φ \to P \in CRing$
57	56	ad2antrr	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to P \in CRing$
58	2 52 57 48 41	crngcomd	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to (f {quot}_{1p} (R) g) \cdot_{P} g = g \cdot_{P} (f {quot}_{1p} (R) g)$
59	58	oveq1d	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to ((f {quot}_{1p} (R) g) \cdot_{P} g) +_{P} (f {rem}_{1p} (R) g) = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} (f {rem}_{1p} (R) g)$
60	55 59	eqtrd	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} (f {rem}_{1p} (R) g)$
61		simpr	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g = Z) \to f {rem}_{1p} (R) g = Z$
62	49 1 2 43 10	r1pdeglt	$⊢ (R \in Ring \land f \in U \land g \in {Unic}_{1p} (R)) \to \deg_{1} (R) (f {rem}_{1p} (R) g) < \deg_{1} (R) (g)$
63	36 37 45 62	syl3anc	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to \deg_{1} (R) (f {rem}_{1p} (R) g) < \deg_{1} (R) (g)$
64	63	adantr	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to \deg_{1} (R) (f {rem}_{1p} (R) g) < \deg_{1} (R) (g)$
65	51	adantr	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to f {rem}_{1p} (R) g \in U$
66		simpr	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to f {rem}_{1p} (R) g \neq Z$
67	65 66	eldifsnd	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to f {rem}_{1p} (R) g \in (U ∖ \{Z\})$
68	67	fvresd	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) = \deg_{1} (R) (f {rem}_{1p} (R) g)$
69		simplr	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to g \in (U ∖ \{Z\})$
70	69	fvresd	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g) = \deg_{1} (R) (g)$
71	64 68 70	3brtr4d	$⊢ (((φ \land f \in U) \land g \in (U ∖ \{Z\})) \land f {rem}_{1p} (R) g \neq Z) \to ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)$
72		exmidne	$⊢ (f {rem}_{1p} (R) g = Z \lor f {rem}_{1p} (R) g \neq Z)$
73	72	a1i	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to (f {rem}_{1p} (R) g = Z \lor f {rem}_{1p} (R) g \neq Z)$
74	61 71 73	orim12da	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to (f {rem}_{1p} (R) g = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))$
75	60 74	jca	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to (f = (g \cdot_{P} (f {quot}_{1p} (R) g)) +_{P} (f {rem}_{1p} (R) g) \land (f {rem}_{1p} (R) g = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (f {rem}_{1p} (R) g) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)))$
76	28 35 48 51 75	2rspcedvdw	$⊢ ((φ \land f \in U) \land g \in (U ∖ \{Z\})) \to \exists q \in U \exists r \in U (f = (g \cdot_{P} q) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)))$
77	76	anasss	$⊢ (φ \land (f \in U \land g \in (U ∖ \{Z\}))) \to \exists q \in U \exists r \in U (f = (g \cdot_{P} q) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)))$
78	77	ralrimivva	$⊢ φ \to \forall f \in U \forall g \in (U ∖ \{Z\}) \exists q \in U \exists r \in U (f = (g \cdot_{P} q) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)))$
79	24 78	jca	$⊢ φ \to (({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) : U ∖ \{Z\} ⟶ ℕ_{0} \land \forall f \in U \forall g \in (U ∖ \{Z\}) \exists q \in U \exists r \in U (f = (g \cdot_{P} q) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g))))$
80	4	reseq1i	$⊢ {\deg_{1} (R) ↾}_{(U ∖ \{Z\})} = {EuclF (P) ↾}_{(U ∖ \{Z\})}$
81	2 3 53 52 80	isedom	$⊢ P \in EDomn \leftrightarrow (P \in IDomn \land (({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) : U ∖ \{Z\} ⟶ ℕ_{0} \land \forall f \in U \forall g \in (U ∖ \{Z\}) \exists q \in U \exists r \in U (f = (g \cdot_{P} q) +_{P} r \land (r = Z \lor ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (r) < ({\deg_{1} (R) ↾}_{(U ∖ \{Z\})}) (g)))))$
82	9 79 81	sylanbrc	$⊢ φ \to P \in EDomn$

Metamath Proof Explorer

Theorem ply1edom

Proof