Metamath Proof Explorer

Definition df-edom

Description: Define Euclidean domains. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Assertion df-edom 
|- EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedom 
 |-  EDomn
1 vd 
 |-  d
2 cidom 
 |-  IDomn
3 ceuf 
 |-  EuclF
4 1 cv 
 |-  d
5 4 3 cfv 
 |-  ( EuclF ` d )
6 ve 
 |-  e
7 cbs 
 |-  Base
8 4 7 cfv 
 |-  ( Base ` d )
9 vv 
 |-  v
10 9 cv 
 |-  v
11 c0g 
 |-  0g
12 4 11 cfv 
 |-  ( 0g ` d )
13 12 csn 
 |-  { ( 0g ` d ) }
14 10 13 cdif 
 |-  ( v \ { ( 0g ` d ) } )
15 vw 
 |-  w
16 6 cv 
 |-  e
17 15 cv 
 |-  w
18 16 17 cres 
 |-  ( e |` w )
19 cn0 
 |-  NN0
20 17 19 18 wf 
 |-  ( e |` w ) : w --> NN0
21 va 
 |-  a
22 vb 
 |-  b
23 vq 
 |-  q
24 vr 
 |-  r
25 21 cv 
 |-  a
26 22 cv 
 |-  b
27 cmulr 
 |-  .r
28 4 27 cfv 
 |-  ( .r ` d )
29 23 cv 
 |-  q
30 26 29 28 co 
 |-  ( b ( .r ` d ) q )
31 cplusg 
 |-  +g
32 4 31 cfv 
 |-  ( +g ` d )
33 24 cv 
 |-  r
34 30 33 32 co 
 |-  ( ( b ( .r ` d ) q ) ( +g ` d ) r )
35 25 34 wceq 
 |-  a = ( ( b ( .r ` d ) q ) ( +g ` d ) r )
36 33 12 wceq 
 |-  r = ( 0g ` d )
37 33 16 cfv 
 |-  ( e ` r )
38 clt 
 |-  <
39 26 16 cfv 
 |-  ( e ` b )
40 37 39 38 wbr 
 |-  ( e ` r ) < ( e ` b )
41 36 40 wo 
 |-  ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) )
42 35 41 wa 
 |-  ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
43 42 24 10 wrex 
 |-  E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
44 43 23 10 wrex 
 |-  E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
45 44 22 17 wral 
 |-  A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
46 45 21 10 wral 
 |-  A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
47 20 46 wa 
 |-  ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) )
48 47 15 14 wsbc 
 |-  [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) )
49 48 9 8 wsbc 
 |-  [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) )
50 49 6 5 wsbc 
 |-  [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) )
51 50 1 2 crab 
 |-  { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) }
52 0 51 wceq 
 |-  EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. a e. v A. b e. w E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) }