Metamath Proof Explorer

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 
|- P = ( Poly1 ` R )
ply1edom.2 
|- U = ( Base ` P )
ply1edom.3 
|- Z = ( 0g ` P )
ply1edom.4 
|- ( deg1 ` R ) = ( EuclF ` P )
ply1edom.5 
|- ( ph -> R e. Field )
Assertion ply1edom 
|- ( ph -> P e. EDomn )

Proof

Step Hyp Ref Expression
1 ply1edom.1 
 |-  P = ( Poly1 ` R )
2 ply1edom.2 
 |-  U = ( Base ` P )
3 ply1edom.3 
 |-  Z = ( 0g ` P )
4 ply1edom.4 
 |-  ( deg1 ` R ) = ( EuclF ` P )
5 ply1edom.5 
 |-  ( ph -> R e. Field )
6 fldidom 
 |-  ( R e. Field -> R e. IDomn )
7 5 6 syl 
 |-  ( ph -> R e. IDomn )
8 1 ply1idom 
 |-  ( R e. IDomn -> P e. IDomn )
9 7 8 syl 
 |-  ( ph -> P e. IDomn )
10 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
11 10 1 2 deg1xrf 
 |-  ( deg1 ` R ) : U --> RR*
12 11 a1i 
 |-  ( ph -> ( deg1 ` R ) : U --> RR* )
13 difssd 
 |-  ( ph -> ( U \ { Z } ) C_ U )
14 nfv 
 |-  F/ f ph
15 12 ffund 
 |-  ( ph -> Fun ( deg1 ` R ) )
16 7 idomringd 
 |-  ( ph -> R e. Ring )
17 16 adantr 
 |-  ( ( ph /\ f e. ( U \ { Z } ) ) -> R e. Ring )
18 13 sselda 
 |-  ( ( ph /\ f e. ( U \ { Z } ) ) -> f e. U )
19 simpr 
 |-  ( ( ph /\ f e. ( U \ { Z } ) ) -> f e. ( U \ { Z } ) )
20 19 eldifsnbd 
 |-  ( ( ph /\ f e. ( U \ { Z } ) ) -> f =/= Z )
21 10 1 3 2 deg1nn0cl 
 |-  ( ( R e. Ring /\ f e. U /\ f =/= Z ) -> ( ( deg1 ` R ) ` f ) e. NN0 )
22 17 18 20 21 syl3anc 
 |-  ( ( ph /\ f e. ( U \ { Z } ) ) -> ( ( deg1 ` R ) ` f ) e. NN0 )
23 14 15 22 funimassd 
 |-  ( ph -> ( ( deg1 ` R ) " ( U \ { Z } ) ) C_ NN0 )
24 12 13 23 fssrescdmd 
 |-  ( ph -> ( ( deg1 ` R ) |` ( U \ { Z } ) ) : ( U \ { Z } ) --> NN0 )
25 oveq2 
 |-  ( q = ( f ( quot1p ` R ) g ) -> ( g ( .r ` P ) q ) = ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) )
26 25 oveq1d 
 |-  ( q = ( f ( quot1p ` R ) g ) -> ( ( g ( .r ` P ) q ) ( +g ` P ) r ) = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) r ) )
27 26 eqeq2d 
 |-  ( q = ( f ( quot1p ` R ) g ) -> ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) <-> f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) r ) ) )
28 27 anbi1d 
 |-  ( q = ( f ( quot1p ` R ) g ) -> ( ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) <-> ( f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) ) )
29 oveq2 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) r ) = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) )
30 29 eqeq2d 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) r ) <-> f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) ) )
31 eqeq1 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( r = Z <-> ( f ( rem1p ` R ) g ) = Z ) )
32 fveq2 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) = ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) )
33 32 breq1d 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) <-> ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) )
34 31 33 orbi12d 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) <-> ( ( f ( rem1p ` R ) g ) = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) )
35 30 34 anbi12d 
 |-  ( r = ( f ( rem1p ` R ) g ) -> ( ( f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) <-> ( f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) /\ ( ( f ( rem1p ` R ) g ) = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) ) )
36 16 ad2antrr 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> R e. Ring )
37 simplr 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> f e. U )
38 5 flddrngd 
 |-  ( ph -> R e. DivRing )
39 38 ad2antrr 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> R e. DivRing )
40 simpr 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> g e. ( U \ { Z } ) )
41 40 eldifad 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> g e. U )
42 40 eldifsnbd 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> g =/= Z )
43 eqid 
 |-  ( Unic1p ` R ) = ( Unic1p ` R )
44 1 2 3 43 drnguc1p 
 |-  ( ( R e. DivRing /\ g e. U /\ g =/= Z ) -> g e. ( Unic1p ` R ) )
45 39 41 42 44 syl3anc 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> g e. ( Unic1p ` R ) )
46 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
47 46 1 2 43 q1pcl 
 |-  ( ( R e. Ring /\ f e. U /\ g e. ( Unic1p ` R ) ) -> ( f ( quot1p ` R ) g ) e. U )
48 36 37 45 47 syl3anc 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( f ( quot1p ` R ) g ) e. U )
49 eqid 
 |-  ( rem1p ` R ) = ( rem1p ` R )
50 49 1 2 43 r1pcl 
 |-  ( ( R e. Ring /\ f e. U /\ g e. ( Unic1p ` R ) ) -> ( f ( rem1p ` R ) g ) e. U )
51 36 37 45 50 syl3anc 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( f ( rem1p ` R ) g ) e. U )
52 eqid 
 |-  ( .r ` P ) = ( .r ` P )
53 eqid 
 |-  ( +g ` P ) = ( +g ` P )
54 1 2 43 46 49 52 53 r1pid 
 |-  ( ( R e. Ring /\ f e. U /\ g e. ( Unic1p ` R ) ) -> f = ( ( ( f ( quot1p ` R ) g ) ( .r ` P ) g ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) )
55 36 37 45 54 syl3anc 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> f = ( ( ( f ( quot1p ` R ) g ) ( .r ` P ) g ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) )
56 9 idomcringd 
 |-  ( ph -> P e. CRing )
57 56 ad2antrr 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> P e. CRing )
58 2 52 57 48 41 crngcomd 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( ( f ( quot1p ` R ) g ) ( .r ` P ) g ) = ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) )
59 58 oveq1d 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( ( ( f ( quot1p ` R ) g ) ( .r ` P ) g ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) )
60 55 59 eqtrd 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) )
61 simpr 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) = Z ) -> ( f ( rem1p ` R ) g ) = Z )
62 49 1 2 43 10 r1pdeglt 
 |-  ( ( R e. Ring /\ f e. U /\ g e. ( Unic1p ` R ) ) -> ( ( deg1 ` R ) ` ( f ( rem1p ` R ) g ) ) < ( ( deg1 ` R ) ` g ) )
63 36 37 45 62 syl3anc 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( ( deg1 ` R ) ` ( f ( rem1p ` R ) g ) ) < ( ( deg1 ` R ) ` g ) )
64 63 adantr 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( ( deg1 ` R ) ` ( f ( rem1p ` R ) g ) ) < ( ( deg1 ` R ) ` g ) )
65 51 adantr 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( f ( rem1p ` R ) g ) e. U )
66 simpr 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( f ( rem1p ` R ) g ) =/= Z )
67 65 66 eldifsnd 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( f ( rem1p ` R ) g ) e. ( U \ { Z } ) )
68 67 fvresd 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) = ( ( deg1 ` R ) ` ( f ( rem1p ` R ) g ) ) )
69 simplr 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> g e. ( U \ { Z } ) )
70 69 fvresd 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) = ( ( deg1 ` R ) ` g ) )
71 64 68 70 3brtr4d 
 |-  ( ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) /\ ( f ( rem1p ` R ) g ) =/= Z ) -> ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) )
72 exmidne 
 |-  ( ( f ( rem1p ` R ) g ) = Z \/ ( f ( rem1p ` R ) g ) =/= Z )
73 72 a1i 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( ( f ( rem1p ` R ) g ) = Z \/ ( f ( rem1p ` R ) g ) =/= Z ) )
74 61 71 73 orim12da 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( ( f ( rem1p ` R ) g ) = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) )
75 60 74 jca 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> ( f = ( ( g ( .r ` P ) ( f ( quot1p ` R ) g ) ) ( +g ` P ) ( f ( rem1p ` R ) g ) ) /\ ( ( f ( rem1p ` R ) g ) = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` ( f ( rem1p ` R ) g ) ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) )
76 28 35 48 51 75 2rspcedvdw 
 |-  ( ( ( ph /\ f e. U ) /\ g e. ( U \ { Z } ) ) -> E. q e. U E. r e. U ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) )
77 76 anasss 
 |-  ( ( ph /\ ( f e. U /\ g e. ( U \ { Z } ) ) ) -> E. q e. U E. r e. U ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) )
78 77 ralrimivva 
 |-  ( ph -> A. f e. U A. g e. ( U \ { Z } ) E. q e. U E. r e. U ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) )
79 24 78 jca 
 |-  ( ph -> ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) : ( U \ { Z } ) --> NN0 /\ A. f e. U A. g e. ( U \ { Z } ) E. q e. U E. r e. U ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) ) )
80 4 reseq1i 
 |-  ( ( deg1 ` R ) |` ( U \ { Z } ) ) = ( ( EuclF ` P ) |` ( U \ { Z } ) )
81 2 3 53 52 80 isedom 
 |-  ( P e. EDomn <-> ( P e. IDomn /\ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) : ( U \ { Z } ) --> NN0 /\ A. f e. U A. g e. ( U \ { Z } ) E. q e. U E. r e. U ( f = ( ( g ( .r ` P ) q ) ( +g ` P ) r ) /\ ( r = Z \/ ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` r ) < ( ( ( deg1 ` R ) |` ( U \ { Z } ) ) ` g ) ) ) ) ) )
82 9 79 81 sylanbrc 
 |-  ( ph -> P e. EDomn )