Metamath Proof Explorer

Theorem fldedom

Description: A field is a Euclidean domain, regardless of its Euclidean norm. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses fldedom.b 
|- B = ( Base ` F )
fldedom.1 
|- .0. = ( 0g ` F )
fldedom.2 
|- W = ( B \ { .0. } )
fldedom.e 
|- E = ( EuclF ` F )
fldedom.f 
|- ( ph -> F e. Field )
fldedom.3 
|- ( ph -> ( E |` W ) : W --> NN0 )
Assertion fldedom 
|- ( ph -> F e. EDomn )

Proof

Step Hyp Ref Expression
1 fldedom.b 
 |-  B = ( Base ` F )
2 fldedom.1 
 |-  .0. = ( 0g ` F )
3 fldedom.2 
 |-  W = ( B \ { .0. } )
4 fldedom.e 
 |-  E = ( EuclF ` F )
5 fldedom.f 
 |-  ( ph -> F e. Field )
6 fldedom.3 
 |-  ( ph -> ( E |` W ) : W --> NN0 )
7 fldidom 
 |-  ( F e. Field -> F e. IDomn )
8 5 7 syl 
 |-  ( ph -> F e. IDomn )
9 3 reseq2i 
 |-  ( E |` W ) = ( E |` ( B \ { .0. } ) )
10 9 a1i 
 |-  ( ph -> ( E |` W ) = ( E |` ( B \ { .0. } ) ) )
11 3 a1i 
 |-  ( ph -> W = ( B \ { .0. } ) )
12 11 6 feq2dd 
 |-  ( ph -> ( E |` W ) : ( B \ { .0. } ) --> NN0 )
13 10 12 feq1dd 
 |-  ( ph -> ( E |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 )
14 oveq2 
 |-  ( q = ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) -> ( y ( .r ` F ) q ) = ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) )
15 14 oveq1d 
 |-  ( q = ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) -> ( ( y ( .r ` F ) q ) ( +g ` F ) r ) = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) r ) )
16 15 eqeq2d 
 |-  ( q = ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) -> ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) <-> x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) r ) ) )
17 16 anbi1d 
 |-  ( q = ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) -> ( ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) <-> ( x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) )
18 oveq2 
 |-  ( r = .0. -> ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) r ) = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) .0. ) )
19 18 eqeq2d 
 |-  ( r = .0. -> ( x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) r ) <-> x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) .0. ) ) )
20 eqeq1 
 |-  ( r = .0. -> ( r = .0. <-> .0. = .0. ) )
21 fveq2 
 |-  ( r = .0. -> ( ( E |` ( B \ { .0. } ) ) ` r ) = ( ( E |` ( B \ { .0. } ) ) ` .0. ) )
22 21 breq1d 
 |-  ( r = .0. -> ( ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) <-> ( ( E |` ( B \ { .0. } ) ) ` .0. ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) )
23 20 22 orbi12d 
 |-  ( r = .0. -> ( ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) <-> ( .0. = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` .0. ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) )
24 19 23 anbi12d 
 |-  ( r = .0. -> ( ( x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) <-> ( x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) .0. ) /\ ( .0. = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` .0. ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) )
25 eqid 
 |-  ( .r ` F ) = ( .r ` F )
26 8 idomringd 
 |-  ( ph -> F e. Ring )
27 26 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> F e. Ring )
28 eqid 
 |-  ( invr ` F ) = ( invr ` F )
29 5 flddrngd 
 |-  ( ph -> F e. DivRing )
30 29 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> F e. DivRing )
31 difssd 
 |-  ( ( ph /\ x e. B ) -> ( B \ { .0. } ) C_ B )
32 31 sselda 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> y e. B )
33 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> y e. ( B \ { .0. } ) )
34 33 eldifsnbd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> y =/= .0. )
35 1 2 28 30 32 34 drnginvrcld 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( ( invr ` F ) ` y ) e. B )
36 simplr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> x e. B )
37 1 25 27 35 36 ringcld 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) e. B )
38 26 ringgrpd 
 |-  ( ph -> F e. Grp )
39 1 2 38 grpidcld 
 |-  ( ph -> .0. e. B )
40 39 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> .0. e. B )
41 eqid 
 |-  ( +g ` F ) = ( +g ` F )
42 38 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> F e. Grp )
43 1 25 27 32 37 ringcld 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) e. B )
44 1 41 2 42 43 grpridd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) .0. ) = ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) )
45 1 25 27 32 35 36 ringassd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( ( y ( .r ` F ) ( ( invr ` F ) ` y ) ) ( .r ` F ) x ) = ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) )
46 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
47 1 2 25 46 28 30 32 34 drnginvrrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( y ( .r ` F ) ( ( invr ` F ) ` y ) ) = ( 1r ` F ) )
48 47 oveq1d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( ( y ( .r ` F ) ( ( invr ` F ) ` y ) ) ( .r ` F ) x ) = ( ( 1r ` F ) ( .r ` F ) x ) )
49 45 48 eqtr3d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) = ( ( 1r ` F ) ( .r ` F ) x ) )
50 1 25 46 27 36 ringlidmd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( ( 1r ` F ) ( .r ` F ) x ) = x )
51 44 49 50 3eqtrrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) .0. ) )
52 eqidd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> .0. = .0. )
53 52 orcd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( .0. = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` .0. ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) )
54 51 53 jca 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> ( x = ( ( y ( .r ` F ) ( ( ( invr ` F ) ` y ) ( .r ` F ) x ) ) ( +g ` F ) .0. ) /\ ( .0. = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` .0. ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) )
55 17 24 37 40 54 2rspcedvdw 
 |-  ( ( ( ph /\ x e. B ) /\ y e. ( B \ { .0. } ) ) -> E. q e. B E. r e. B ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) )
56 55 anasss 
 |-  ( ( ph /\ ( x e. B /\ y e. ( B \ { .0. } ) ) ) -> E. q e. B E. r e. B ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) )
57 56 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) )
58 13 57 jca 
 |-  ( ph -> ( ( E |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) )
59 4 reseq1i 
 |-  ( E |` ( B \ { .0. } ) ) = ( ( EuclF ` F ) |` ( B \ { .0. } ) )
60 1 2 41 25 59 isedom 
 |-  ( F e. EDomn <-> ( F e. IDomn /\ ( ( E |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` F ) q ) ( +g ` F ) r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) ) )
61 8 58 60 sylanbrc 
 |-  ( ph -> F e. EDomn )