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 ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) 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 6 cv 
 |-  e
11 10 wfun 
 |-  Fun e
12 9 cv 
 |-  v
13 c0g 
 |-  0g
14 4 13 cfv 
 |-  ( 0g ` d )
15 14 csn 
 |-  { ( 0g ` d ) }
16 12 15 cdif 
 |-  ( v \ { ( 0g ` d ) } )
17 10 16 cima 
 |-  ( e " ( v \ { ( 0g ` d ) } ) )
18 cc0 
 |-  0
19 cico 
 |-  [,)
20 cpnf 
 |-  +oo
21 18 20 19 co 
 |-  ( 0 [,) +oo )
22 17 21 wss 
 |-  ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo )
23 va 
 |-  a
24 vb 
 |-  b
25 vq 
 |-  q
26 vr 
 |-  r
27 23 cv 
 |-  a
28 24 cv 
 |-  b
29 cmulr 
 |-  .r
30 4 29 cfv 
 |-  ( .r ` d )
31 25 cv 
 |-  q
32 28 31 30 co 
 |-  ( b ( .r ` d ) q )
33 cplusg 
 |-  +g
34 4 33 cfv 
 |-  ( +g ` d )
35 26 cv 
 |-  r
36 32 35 34 co 
 |-  ( ( b ( .r ` d ) q ) ( +g ` d ) r )
37 27 36 wceq 
 |-  a = ( ( b ( .r ` d ) q ) ( +g ` d ) r )
38 35 14 wceq 
 |-  r = ( 0g ` d )
39 35 10 cfv 
 |-  ( e ` r )
40 clt 
 |-  <
41 28 10 cfv 
 |-  ( e ` b )
42 39 41 40 wbr 
 |-  ( e ` r ) < ( e ` b )
43 38 42 wo 
 |-  ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) )
44 37 43 wa 
 |-  ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
45 44 26 12 wrex 
 |-  E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
46 45 25 12 wrex 
 |-  E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
47 46 24 16 wral 
 |-  A. b e. ( v \ { ( 0g ` d ) } ) 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 23 12 wral 
 |-  A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) )
49 11 22 48 w3a 
 |-  ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) 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 9 8 wsbc 
 |-  [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) 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 6 5 wsbc 
 |-  [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) )
52 51 1 2 crab 
 |-  { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) }
53 0 52 wceq 
 |-  EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) }