Metamath Proof Explorer

Theorem edomediv

Description: Apply a Euclidean division in a Euclidean domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses edomediv.b 
|- B = ( Base ` D )
edomediv.z 
|- .0. = ( 0g ` D )
edomediv.p 
|- .+ = ( +g ` D )
edomediv.m 
|- .x. = ( .r ` D )
edomediv.e 
|- E = ( EuclF ` D )
edomediv.d 
|- ( ph -> D e. EDomn )
edomediv.x 
|- ( ph -> X e. B )
edomediv.y 
|- ( ph -> Y e. ( B \ { .0. } ) )
Assertion edomediv 
|- ( ph -> 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 edomediv.b 
 |-  B = ( Base ` D )
2 edomediv.z 
 |-  .0. = ( 0g ` D )
3 edomediv.p 
 |-  .+ = ( +g ` D )
4 edomediv.m 
 |-  .x. = ( .r ` D )
5 edomediv.e 
 |-  E = ( EuclF ` D )
6 edomediv.d 
 |-  ( ph -> D e. EDomn )
7 edomediv.x 
 |-  ( ph -> X e. B )
8 edomediv.y 
 |-  ( ph -> Y e. ( B \ { .0. } ) )
9 eqeq1 
 |-  ( x = X -> ( x = ( ( y .x. q ) .+ r ) <-> X = ( ( y .x. q ) .+ r ) ) )
10 9 anbi1d 
 |-  ( x = X -> ( ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) <-> ( X = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) )
11 10 2rexbidv 
 |-  ( x = X -> ( E. q e. B E. r e. B ( x = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) <-> E. q e. B E. r e. B ( X = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) )
12 oveq1 
 |-  ( y = Y -> ( y .x. q ) = ( Y .x. q ) )
13 12 oveq1d 
 |-  ( y = Y -> ( ( y .x. q ) .+ r ) = ( ( Y .x. q ) .+ r ) )
14 13 eqeq2d 
 |-  ( y = Y -> ( X = ( ( y .x. q ) .+ r ) <-> X = ( ( Y .x. q ) .+ r ) ) )
15 fveq2 
 |-  ( y = Y -> ( ( E |` ( B \ { .0. } ) ) ` y ) = ( ( E |` ( B \ { .0. } ) ) ` Y ) )
16 15 breq2d 
 |-  ( y = Y -> ( ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) <-> ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) )
17 16 orbi2d 
 |-  ( y = Y -> ( ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) <-> ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) )
18 14 17 anbi12d 
 |-  ( y = Y -> ( ( X = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) <-> ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) ) )
19 18 2rexbidv 
 |-  ( y = Y -> ( E. q e. B E. r e. B ( X = ( ( y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) <-> E. q e. B E. r e. B ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) ) )
20 5 reseq1i 
 |-  ( E |` ( B \ { .0. } ) ) = ( ( EuclF ` D ) |` ( B \ { .0. } ) )
21 1 2 3 4 20 isedom 
 |-  ( D e. EDomn <-> ( D 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 .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) ) )
22 6 21 sylib 
 |-  ( ph -> ( D 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 .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) ) ) )
23 22 simprrd 
 |-  ( ph -> 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 |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` y ) ) ) )
24 11 19 23 7 8 rspc2dv 
 |-  ( ph -> E. q e. B E. r e. B ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) )
25 biort 
 |-  ( r = .0. -> ( r = .0. <-> ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) )
26 biort 
 |-  ( r = .0. -> ( r = .0. <-> ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) )
27 25 26 bitr3d 
 |-  ( r = .0. -> ( ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) )
28 27 adantl 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r = .0. ) -> ( ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) )
29 simplr 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> r e. B )
30 simpr 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> r =/= .0. )
31 29 30 eldifsnd 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> r e. ( B \ { .0. } ) )
32 31 fvresd 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) ` r ) = ( E ` r ) )
33 8 ad2antrr 
 |-  ( ( ( ph /\ q e. B ) /\ r e. B ) -> Y e. ( B \ { .0. } ) )
34 33 fvresd 
 |-  ( ( ( ph /\ q e. B ) /\ r e. B ) -> ( ( E |` ( B \ { .0. } ) ) ` Y ) = ( E ` Y ) )
35 34 adantr 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> ( ( E |` ( B \ { .0. } ) ) ` Y ) = ( E ` Y ) )
36 32 35 breq12d 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> ( ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) <-> ( E ` r ) < ( E ` Y ) ) )
37 36 orbi2d 
 |-  ( ( ( ( ph /\ q e. B ) /\ r e. B ) /\ r =/= .0. ) -> ( ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) )
38 28 37 pm2.61dane 
 |-  ( ( ( ph /\ q e. B ) /\ r e. B ) -> ( ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) <-> ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) )
39 38 anbi2d 
 |-  ( ( ( ph /\ q e. B ) /\ r e. B ) -> ( ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) <-> ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) ) )
40 39 anasss 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) <-> ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) ) )
41 40 2rexbidva 
 |-  ( ph -> ( E. q e. B E. r e. B ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( ( E |` ( B \ { .0. } ) ) ` r ) < ( ( E |` ( B \ { .0. } ) ) ` Y ) ) ) <-> E. q e. B E. r e. B ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) ) )
42 24 41 mpbid 
 |-  ( ph -> E. q e. B E. r e. B ( X = ( ( Y .x. q ) .+ r ) /\ ( r = .0. \/ ( E ` r ) < ( E ` Y ) ) ) )