Metamath Proof Explorer

Theorem isedom

Description: Property of being a Euclidean domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses isedom.b 
|- B = ( Base ` D )
isedom.0 
|- .0. = ( 0g ` D )
isedom.p 
|- .+ = ( +g ` D )
isedom.m 
|- .x. = ( .r ` D )
isedom.e 
|- E = ( ( EuclF ` D ) |` ( B \ { .0. } ) )
Assertion isedom 
|- ( D e. EDomn <-> ( D e. IDomn /\ ( E : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isedom.b 
 |-  B = ( Base ` D )
2 isedom.0 
 |-  .0. = ( 0g ` D )
3 isedom.p 
 |-  .+ = ( +g ` D )
4 isedom.m 
 |-  .x. = ( .r ` D )
5 isedom.e 
 |-  E = ( ( EuclF ` D ) |` ( B \ { .0. } ) )
6 eqid 
 |-  ( EuclF ` D ) = ( EuclF ` D )
7 vex 
 |-  v e. _V
8 7 difexi 
 |-  ( v \ { ( 0g ` d ) } ) e. _V
9 8 a1i 
 |-  ( ( e = ( EuclF ` D ) /\ v = B ) -> ( v \ { ( 0g ` d ) } ) e. _V )
10 simpll 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> e = ( EuclF ` D ) )
11 simpr 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> w = ( v \ { ( 0g ` d ) } ) )
12 simplr 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> v = B )
13 12 difeq1d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( v \ { ( 0g ` d ) } ) = ( B \ { ( 0g ` d ) } ) )
14 11 13 eqtrd 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> w = ( B \ { ( 0g ` d ) } ) )
15 10 14 reseq12d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( e |` w ) = ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) )
16 15 14 feq12d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( ( e |` w ) : w --> NN0 <-> ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) : ( B \ { ( 0g ` d ) } ) --> NN0 ) )
17 10 fveq1d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( e ` r ) = ( ( EuclF ` D ) ` r ) )
18 10 fveq1d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( e ` y ) = ( ( EuclF ` D ) ` y ) )
19 17 18 breq12d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( ( e ` r ) < ( e ` y ) <-> ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) )
20 19 orbi2d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) <-> ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) )
21 20 anbi2d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) <-> ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) )
22 12 21 rexeqbidv 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) <-> E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) )
23 12 22 rexeqbidv 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) <-> E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) )
24 14 23 raleqbidv 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) <-> A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) )
25 12 24 raleqbidv 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( A. x e. v A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) <-> A. x e. B A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) )
26 16 25 anbi12d 
 |-  ( ( ( e = ( EuclF ` D ) /\ v = B ) /\ w = ( v \ { ( 0g ` d ) } ) ) -> ( ( ( e |` w ) : w --> NN0 /\ A. x e. v A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) ) <-> ( ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) : ( B \ { ( 0g ` d ) } ) --> NN0 /\ A. x e. B A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) ) )
27 9 26 sbcied 
 |-  ( ( e = ( EuclF ` D ) /\ v = B ) -> ( [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. x e. v A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) ) <-> ( ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) : ( B \ { ( 0g ` d ) } ) --> NN0 /\ A. x e. B A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) ) )
28 6 1 27 sbcie2s 
 |-  ( d = D -> ( [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. x e. v A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) ) <-> ( ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) : ( B \ { ( 0g ` d ) } ) --> NN0 /\ A. x e. B A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) ) )
29 fveq2 
 |-  ( d = D -> ( 0g ` d ) = ( 0g ` D ) )
30 29 2 eqtr4di 
 |-  ( d = D -> ( 0g ` d ) = .0. )
31 30 sneqd 
 |-  ( d = D -> { ( 0g ` d ) } = { .0. } )
32 31 difeq2d 
 |-  ( d = D -> ( B \ { ( 0g ` d ) } ) = ( B \ { .0. } ) )
33 32 reseq2d 
 |-  ( d = D -> ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) = ( ( EuclF ` D ) |` ( B \ { .0. } ) ) )
34 33 5 eqtr4di 
 |-  ( d = D -> ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) = E )
35 34 32 feq12d 
 |-  ( d = D -> ( ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) : ( B \ { ( 0g ` d ) } ) --> NN0 <-> E : ( B \ { .0. } ) --> NN0 ) )
36 fveq2 
 |-  ( d = D -> ( +g ` d ) = ( +g ` D ) )
37 36 3 eqtr4di 
 |-  ( d = D -> ( +g ` d ) = .+ )
38 fveq2 
 |-  ( d = D -> ( .r ` d ) = ( .r ` D ) )
39 38 4 eqtr4di 
 |-  ( d = D -> ( .r ` d ) = .x. )
40 39 oveqd 
 |-  ( d = D -> ( y ( .r ` d ) q ) = ( y .x. q ) )
41 eqidd 
 |-  ( d = D -> r = r )
42 37 40 41 oveq123d 
 |-  ( d = D -> ( ( y ( .r ` d ) q ) ( +g ` d ) r ) = ( ( y .x. q ) .+ r ) )
43 42 eqeq2d 
 |-  ( d = D -> ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) <-> x = ( ( y .x. q ) .+ r ) ) )
44 43 ad2antrr 
 |-  ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) -> ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) <-> x = ( ( y .x. q ) .+ r ) ) )
45 30 eqeq2d 
 |-  ( d = D -> ( r = ( 0g ` d ) <-> r = .0. ) )
46 45 ad2antrr 
 |-  ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) -> ( r = ( 0g ` d ) <-> r = .0. ) )
47 46 orbi1d 
 |-  ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) -> ( ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) <-> ( r = .0. \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) )
48 biort 
 |-  ( r = .0. -> ( r = .0. <-> ( r = .0. \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) )
49 biort 
 |-  ( r = .0. -> ( r = .0. <-> ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) )
50 48 49 bitr3d 
 |-  ( r = .0. -> ( ( r = .0. \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) )
51 50 adantl 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r = .0. ) -> ( ( r = .0. \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) )
52 5 fveq1i 
 |-  ( E ` r ) = ( ( ( EuclF ` D ) |` ( B \ { .0. } ) ) ` r )
53 simplr 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> r e. B )
54 simpr 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> r =/= .0. )
55 53 54 eldifsnd 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> r e. ( B \ { .0. } ) )
56 55 fvresd 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> ( ( ( EuclF ` D ) |` ( B \ { .0. } ) ) ` r ) = ( ( EuclF ` D ) ` r ) )
57 52 56 eqtr2id 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> ( ( EuclF ` D ) ` r ) = ( E ` r ) )
58 5 fveq1i 
 |-  ( E ` y ) = ( ( ( EuclF ` D ) |` ( B \ { .0. } ) ) ` y )
59 simpr 
 |-  ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) -> y e. ( B \ { ( 0g ` d ) } ) )
60 32 adantr 
 |-  ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) -> ( B \ { ( 0g ` d ) } ) = ( B \ { .0. } ) )
61 59 60 eleqtrd 
 |-  ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) -> y e. ( B \ { .0. } ) )
62 61 ad2antrr 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> y e. ( B \ { .0. } ) )
63 62 fvresd 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> ( ( ( EuclF ` D ) |` ( B \ { .0. } ) ) ` y ) = ( ( EuclF ` D ) ` y ) )
64 58 63 eqtr2id 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> ( ( EuclF ` D ) ` y ) = ( E ` y ) )
65 57 64 breq12d 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> ( ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) <-> ( E ` r ) < ( E ` y ) ) )
66 65 orbi2d 
 |-  ( ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) /\ r =/= .0. ) -> ( ( r = .0. \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) )
67 51 66 pm2.61dane 
 |-  ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) -> ( ( r = .0. \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) )
68 47 67 bitrd 
 |-  ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) -> ( ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) )
69 44 68 anbi12d 
 |-  ( ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) /\ r e. B ) -> ( ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) <-> ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) )
70 69 rexbidva 
 |-  ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) -> ( E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) <-> E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) )
71 70 rexbidv 
 |-  ( ( d = D /\ y e. ( B \ { ( 0g ` d ) } ) ) -> ( E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) <-> E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) )
72 32 71 raleqbidva 
 |-  ( d = D -> ( A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) <-> A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) )
73 72 ralbidv 
 |-  ( d = D -> ( A. x e. B A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) <-> A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) )
74 35 73 anbi12d 
 |-  ( d = D -> ( ( ( ( EuclF ` D ) |` ( B \ { ( 0g ` d ) } ) ) : ( B \ { ( 0g ` d ) } ) --> NN0 /\ A. x e. B A. y e. ( B \ { ( 0g ` d ) } ) E. q e. B E. r e. B ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( ( EuclF ` D ) ` r ) < ( ( EuclF ` D ) ` y ) ) ) ) <-> ( E : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) ) )
75 28 74 bitrd 
 |-  ( d = D -> ( [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. x e. v A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) ) <-> ( E : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) ) )
76 df-edom 
 |-  EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. [. ( v \ { ( 0g ` d ) } ) / w ]. ( ( e |` w ) : w --> NN0 /\ A. x e. v A. y e. w E. q e. v E. r e. v ( x = ( ( y ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` y ) ) ) ) }
77 75 76 elrab2 
 |-  ( D e. EDomn <-> ( D e. IDomn /\ ( E : ( B \ { .0. } ) --> NN0 /\ A. x e. B A. y e. ( B \ { .0. } ) E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` y ) ) ) ) ) )