Metamath Proof Explorer

Theorem dvdsruassoi

Description: If two elements X and Y of a ring R are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses dvdsrspss.b 
|- B = ( Base ` R )
dvdsrspss.k 
|- K = ( RSpan ` R )
dvdsrspss.d 
|- .|| = ( ||r ` R )
dvdsrspss.x 
|- ( ph -> X e. B )
dvdsrspss.y 
|- ( ph -> Y e. B )
dvdsruassoi.1 
|- U = ( Unit ` R )
dvdsruassoi.2 
|- .x. = ( .r ` R )
dvdsruassoi.r 
|- ( ph -> R e. Ring )
dvdsruassoi.3 
|- ( ph -> V e. U )
dvdsruassoi.4 
|- ( ph -> ( V .x. X ) = Y )
Assertion dvdsruassoi 
|- ( ph -> ( X .|| Y /\ Y .|| X ) )

Proof

Step Hyp Ref Expression
1 dvdsrspss.b 
 |-  B = ( Base ` R )
2 dvdsrspss.k 
 |-  K = ( RSpan ` R )
3 dvdsrspss.d 
 |-  .|| = ( ||r ` R )
4 dvdsrspss.x 
 |-  ( ph -> X e. B )
5 dvdsrspss.y 
 |-  ( ph -> Y e. B )
6 dvdsruassoi.1 
 |-  U = ( Unit ` R )
7 dvdsruassoi.2 
 |-  .x. = ( .r ` R )
8 dvdsruassoi.r 
 |-  ( ph -> R e. Ring )
9 dvdsruassoi.3 
 |-  ( ph -> V e. U )
10 dvdsruassoi.4 
 |-  ( ph -> ( V .x. X ) = Y )
11 1 6 unitss 
 |-  U C_ B
12 11 9 sselid 
 |-  ( ph -> V e. B )
13 oveq1 
 |-  ( t = V -> ( t .x. X ) = ( V .x. X ) )
14 13 eqeq1d 
 |-  ( t = V -> ( ( t .x. X ) = Y <-> ( V .x. X ) = Y ) )
15 14 adantl 
 |-  ( ( ph /\ t = V ) -> ( ( t .x. X ) = Y <-> ( V .x. X ) = Y ) )
16 12 15 10 rspcedvd 
 |-  ( ph -> E. t e. B ( t .x. X ) = Y )
17 eqid 
 |-  ( invr ` R ) = ( invr ` R )
18 6 17 1 ringinvcl 
 |-  ( ( R e. Ring /\ V e. U ) -> ( ( invr ` R ) ` V ) e. B )
19 8 9 18 syl2anc 
 |-  ( ph -> ( ( invr ` R ) ` V ) e. B )
20 oveq1 
 |-  ( s = ( ( invr ` R ) ` V ) -> ( s .x. Y ) = ( ( ( invr ` R ) ` V ) .x. Y ) )
21 20 eqeq1d 
 |-  ( s = ( ( invr ` R ) ` V ) -> ( ( s .x. Y ) = X <-> ( ( ( invr ` R ) ` V ) .x. Y ) = X ) )
22 21 adantl 
 |-  ( ( ph /\ s = ( ( invr ` R ) ` V ) ) -> ( ( s .x. Y ) = X <-> ( ( ( invr ` R ) ` V ) .x. Y ) = X ) )
23 1 7 8 19 12 4 ringassd 
 |-  ( ph -> ( ( ( ( invr ` R ) ` V ) .x. V ) .x. X ) = ( ( ( invr ` R ) ` V ) .x. ( V .x. X ) ) )
24 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
25 6 17 7 24 unitlinv 
 |-  ( ( R e. Ring /\ V e. U ) -> ( ( ( invr ` R ) ` V ) .x. V ) = ( 1r ` R ) )
26 8 9 25 syl2anc 
 |-  ( ph -> ( ( ( invr ` R ) ` V ) .x. V ) = ( 1r ` R ) )
27 26 oveq1d 
 |-  ( ph -> ( ( ( ( invr ` R ) ` V ) .x. V ) .x. X ) = ( ( 1r ` R ) .x. X ) )
28 1 7 24 8 4 ringlidmd 
 |-  ( ph -> ( ( 1r ` R ) .x. X ) = X )
29 27 28 eqtrd 
 |-  ( ph -> ( ( ( ( invr ` R ) ` V ) .x. V ) .x. X ) = X )
30 10 oveq2d 
 |-  ( ph -> ( ( ( invr ` R ) ` V ) .x. ( V .x. X ) ) = ( ( ( invr ` R ) ` V ) .x. Y ) )
31 23 29 30 3eqtr3rd 
 |-  ( ph -> ( ( ( invr ` R ) ` V ) .x. Y ) = X )
32 19 22 31 rspcedvd 
 |-  ( ph -> E. s e. B ( s .x. Y ) = X )
33 1 3 7 dvdsr 
 |-  ( X .|| Y <-> ( X e. B /\ E. t e. B ( t .x. X ) = Y ) )
34 4 biantrurd 
 |-  ( ph -> ( E. t e. B ( t .x. X ) = Y <-> ( X e. B /\ E. t e. B ( t .x. X ) = Y ) ) )
35 33 34 bitr4id 
 |-  ( ph -> ( X .|| Y <-> E. t e. B ( t .x. X ) = Y ) )
36 1 3 7 dvdsr 
 |-  ( Y .|| X <-> ( Y e. B /\ E. s e. B ( s .x. Y ) = X ) )
37 5 biantrurd 
 |-  ( ph -> ( E. s e. B ( s .x. Y ) = X <-> ( Y e. B /\ E. s e. B ( s .x. Y ) = X ) ) )
38 36 37 bitr4id 
 |-  ( ph -> ( Y .|| X <-> E. s e. B ( s .x. Y ) = X ) )
39 35 38 anbi12d 
 |-  ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> ( E. t e. B ( t .x. X ) = Y /\ E. s e. B ( s .x. Y ) = X ) ) )
40 16 32 39 mpbir2and 
 |-  ( ph -> ( X .|| Y /\ Y .|| X ) )