Theorem 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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1edom.2	⊢ 𝑈 = ( Base ‘ 𝑃 )
	ply1edom.3	⊢ 𝑍 = ( 0g ‘ 𝑃 )
	ply1edom.4	⊢ ( deg1 ‘ 𝑅 ) = ( EuclF ‘ 𝑃 )
	ply1edom.5	⊢ ( 𝜑 → 𝑅 ∈ Field )
Assertion	ply1edom	⊢ ( 𝜑 → 𝑃 ∈ EDomn )

Proof

Step	Hyp	Ref	Expression
1		ply1edom.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1edom.2	⊢ 𝑈 = ( Base ‘ 𝑃 )
3		ply1edom.3	⊢ 𝑍 = ( 0g ‘ 𝑃 )
4		ply1edom.4	⊢ ( deg1 ‘ 𝑅 ) = ( EuclF ‘ 𝑃 )
5		ply1edom.5	⊢ ( 𝜑 → 𝑅 ∈ Field )
6		fldidom	⊢ ( 𝑅 ∈ Field → 𝑅 ∈ IDomn )
7	5 6	syl	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
8	1	ply1idom	⊢ ( 𝑅 ∈ IDomn → 𝑃 ∈ IDomn )
9	7 8	syl	⊢ ( 𝜑 → 𝑃 ∈ IDomn )
10		eqid	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
11	10 1 2	deg1xrf	⊢ ( deg1 ‘ 𝑅 ) : 𝑈 ⟶ ℝ*
12	11	a1i	⊢ ( 𝜑 → ( deg1 ‘ 𝑅 ) : 𝑈 ⟶ ℝ* )
13		difssd	⊢ ( 𝜑 → ( 𝑈 ∖ { 𝑍 } ) ⊆ 𝑈 )
14		nfv	⊢ Ⅎ 𝑓 𝜑
15	12	ffund	⊢ ( 𝜑 → Fun ( deg1 ‘ 𝑅 ) )
16	7	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑅 ∈ Ring )
18	13	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑓 ∈ 𝑈 )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑓 ∈ ( 𝑈 ∖ { 𝑍 } ) )
20	19	eldifsnbd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑓 ≠ 𝑍 )
21	10 1 3 2	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑓 ≠ 𝑍 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ∈ ℕ0 )
22	17 18 20 21	syl3anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ∈ ℕ0 )
23	14 15 22	funimassd	⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) “ ( 𝑈 ∖ { 𝑍 } ) ) ⊆ ℕ0 )
24	12 13 23	fssrescdmd	⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) : ( 𝑈 ∖ { 𝑍 } ) ⟶ ℕ0 )
25		oveq2	⊢ ( 𝑞 = ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) → ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) = ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) )
26	25	oveq1d	⊢ ( 𝑞 = ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) → ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) 𝑟 ) )
27	26	eqeq2d	⊢ ( 𝑞 = ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) → ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ↔ 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) 𝑟 ) ) )
28	27	anbi1d	⊢ ( 𝑞 = ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) → ( ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) ↔ ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) ) )
29		oveq2	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) 𝑟 ) = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
30	29	eqeq2d	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) 𝑟 ) ↔ 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) ) )
31		eqeq1	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( 𝑟 = 𝑍 ↔ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ) )
32		fveq2	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) = ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
33	32	breq1d	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ↔ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) )
34	31 33	orbi12d	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ↔ ( ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) )
35	30 34	anbi12d	⊢ ( 𝑟 = ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) → ( ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) ↔ ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) ∧ ( ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) ) )
36	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑅 ∈ Ring )
37		simplr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑓 ∈ 𝑈 )
38	5	flddrngd	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
39	38	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑅 ∈ DivRing )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) )
41	40	eldifad	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑔 ∈ 𝑈 )
42	40	eldifsnbd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑔 ≠ 𝑍 )
43		eqid	⊢ ( Unic1p ‘ 𝑅 ) = ( Unic1p ‘ 𝑅 )
44	1 2 3 43	drnguc1p	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑔 ∈ 𝑈 ∧ 𝑔 ≠ 𝑍 ) → 𝑔 ∈ ( Unic1p ‘ 𝑅 ) )
45	39 41 42 44	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑔 ∈ ( Unic1p ‘ 𝑅 ) )
46		eqid	⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
47	46 1 2 43	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑔 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ∈ 𝑈 )
48	36 37 45 47	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ∈ 𝑈 )
49		eqid	⊢ ( rem1p ‘ 𝑅 ) = ( rem1p ‘ 𝑅 )
50	49 1 2 43	r1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑔 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ∈ 𝑈 )
51	36 37 45 50	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ∈ 𝑈 )
52		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
53		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
54	1 2 43 46 49 52 53	r1pid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑔 ∈ ( Unic1p ‘ 𝑅 ) ) → 𝑓 = ( ( ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ( .r ‘ 𝑃 ) 𝑔 ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
55	36 37 45 54	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑓 = ( ( ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ( .r ‘ 𝑃 ) 𝑔 ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
56	9	idomcringd	⊢ ( 𝜑 → 𝑃 ∈ CRing )
57	56	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑃 ∈ CRing )
58	2 52 57 48 41	crngcomd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ( .r ‘ 𝑃 ) 𝑔 ) = ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) )
59	58	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( ( ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ( .r ‘ 𝑃 ) 𝑔 ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
60	55 59	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
61		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ) → ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 )
62	49 1 2 43 10	r1pdeglt	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑔 ∈ ( Unic1p ‘ 𝑅 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) )
63	36 37 45 62	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) )
64	63	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) )
65	51	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ∈ 𝑈 )
66		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 )
67	65 66	eldifsnd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ∈ ( 𝑈 ∖ { 𝑍 } ) )
68	67	fvresd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) )
69		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) )
70	69	fvresd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) )
71	64 68 70	3brtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ∧ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) → ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) )
72		exmidne	⊢ ( ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ∨ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 )
73	72	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ∨ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ≠ 𝑍 ) )
74	61 71 73	orim12da	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) )
75	60 74	jca	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) ( 𝑓 ( quot1p ‘ 𝑅 ) 𝑔 ) ) ( +g ‘ 𝑃 ) ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) ∧ ( ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ ( 𝑓 ( rem1p ‘ 𝑅 ) 𝑔 ) ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) )
76	28 35 48 51 75	2rspcedvdw	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) → ∃ 𝑞 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) )
77	76	anasss	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑈 ∧ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ) ) → ∃ 𝑞 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) )
78	77	ralrimivva	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑈 ∀ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ∃ 𝑞 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) )
79	24 78	jca	⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) : ( 𝑈 ∖ { 𝑍 } ) ⟶ ℕ0 ∧ ∀ 𝑓 ∈ 𝑈 ∀ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ∃ 𝑞 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) ) )
80	4	reseq1i	⊢ ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) = ( ( EuclF ‘ 𝑃 ) ↾ ( 𝑈 ∖ { 𝑍 } ) )
81	2 3 53 52 80	isedom	⊢ ( 𝑃 ∈ EDomn ↔ ( 𝑃 ∈ IDomn ∧ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) : ( 𝑈 ∖ { 𝑍 } ) ⟶ ℕ0 ∧ ∀ 𝑓 ∈ 𝑈 ∀ 𝑔 ∈ ( 𝑈 ∖ { 𝑍 } ) ∃ 𝑞 ∈ 𝑈 ∃ 𝑟 ∈ 𝑈 ( 𝑓 = ( ( 𝑔 ( .r ‘ 𝑃 ) 𝑞 ) ( +g ‘ 𝑃 ) 𝑟 ) ∧ ( 𝑟 = 𝑍 ∨ ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑟 ) < ( ( ( deg1 ‘ 𝑅 ) ↾ ( 𝑈 ∖ { 𝑍 } ) ) ‘ 𝑔 ) ) ) ) ) )
82	9 79 81	sylanbrc	⊢ ( 𝜑 → 𝑃 ∈ EDomn )