This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsruasso

Description: Two elements X and Y of a ring R are associates, i.e. each divides the other, iff they are unit multiples of each 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 )
dvdsruasso.r 
|- ( ph -> R e. IDomn )
Assertion dvdsruasso 
|- ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> E. u e. U ( u .x. X ) = Y ) )

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 dvdsruasso.r 
 |-  ( ph -> R e. IDomn )
9 1 3 7 dvdsr 
 |-  ( X .|| Y <-> ( X e. B /\ E. t e. B ( t .x. X ) = Y ) )
10 4 biantrurd 
 |-  ( ph -> ( E. t e. B ( t .x. X ) = Y <-> ( X e. B /\ E. t e. B ( t .x. X ) = Y ) ) )
11 9 10 bitr4id 
 |-  ( ph -> ( X .|| Y <-> E. t e. B ( t .x. X ) = Y ) )
12 1 3 7 dvdsr 
 |-  ( Y .|| X <-> ( Y e. B /\ E. s e. B ( s .x. Y ) = X ) )
13 5 biantrurd 
 |-  ( ph -> ( E. s e. B ( s .x. Y ) = X <-> ( Y e. B /\ E. s e. B ( s .x. Y ) = X ) ) )
14 12 13 bitr4id 
 |-  ( ph -> ( Y .|| X <-> E. s e. B ( s .x. Y ) = X ) )
15 11 14 anbi12d 
 |-  ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> ( E. t e. B ( t .x. X ) = Y /\ E. s e. B ( s .x. Y ) = X ) ) )
16 8 idomringd 
 |-  ( ph -> R e. Ring )
17 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
18 6 17 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
19 16 18 syl 
 |-  ( ph -> ( 1r ` R ) e. U )
20 19 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( 1r ` R ) e. U )
21 oveq1 
 |-  ( u = ( 1r ` R ) -> ( u .x. X ) = ( ( 1r ` R ) .x. X ) )
22 21 eqeq1d 
 |-  ( u = ( 1r ` R ) -> ( ( u .x. X ) = Y <-> ( ( 1r ` R ) .x. X ) = Y ) )
23 22 adantl 
 |-  ( ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) /\ u = ( 1r ` R ) ) -> ( ( u .x. X ) = Y <-> ( ( 1r ` R ) .x. X ) = Y ) )
24 16 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> R e. Ring )
25 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> X e. B )
26 1 7 17 24 25 ringlidmd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( ( 1r ` R ) .x. X ) = X )
27 simpr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> X = ( 0g ` R ) )
28 27 oveq2d 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( t .x. X ) = ( t .x. ( 0g ` R ) ) )
29 simplr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( t .x. X ) = Y )
30 simpllr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> t e. B )
31 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
32 1 7 31 ringrz 
 |-  ( ( R e. Ring /\ t e. B ) -> ( t .x. ( 0g ` R ) ) = ( 0g ` R ) )
33 24 30 32 syl2anc 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( t .x. ( 0g ` R ) ) = ( 0g ` R ) )
34 28 29 33 3eqtr3rd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( 0g ` R ) = Y )
35 26 27 34 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> ( ( 1r ` R ) .x. X ) = Y )
36 20 23 35 rspcedvd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X = ( 0g ` R ) ) -> E. u e. U ( u .x. X ) = Y )
37 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
38 8 37 sylib 
 |-  ( ph -> ( R e. CRing /\ R e. Domn ) )
39 38 simpld 
 |-  ( ph -> R e. CRing )
40 39 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> R e. CRing )
41 simp-5r 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> s e. B )
42 simpllr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> t e. B )
43 16 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> R e. Ring )
44 1 7 43 41 42 ringcld 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( s .x. t ) e. B )
45 1 17 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
46 43 45 syl 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( 1r ` R ) e. B )
47 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> X e. B )
48 simpr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> X =/= ( 0g ` R ) )
49 eldifsn 
 |-  ( X e. ( B \ { ( 0g ` R ) } ) <-> ( X e. B /\ X =/= ( 0g ` R ) ) )
50 47 48 49 sylanbrc 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> X e. ( B \ { ( 0g ` R ) } ) )
51 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> R e. IDomn )
52 simplr 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( t .x. X ) = Y )
53 52 oveq2d 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( s .x. ( t .x. X ) ) = ( s .x. Y ) )
54 simp-4r 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( s .x. Y ) = X )
55 53 54 eqtrd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( s .x. ( t .x. X ) ) = X )
56 1 7 43 41 42 47 ringassd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( ( s .x. t ) .x. X ) = ( s .x. ( t .x. X ) ) )
57 1 7 17 43 47 ringlidmd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( ( 1r ` R ) .x. X ) = X )
58 55 56 57 3eqtr4d 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( ( s .x. t ) .x. X ) = ( ( 1r ` R ) .x. X ) )
59 1 31 7 44 46 50 51 58 idomrcan 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( s .x. t ) = ( 1r ` R ) )
60 43 18 syl 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( 1r ` R ) e. U )
61 59 60 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> ( s .x. t ) e. U )
62 6 7 1 unitmulclb 
 |-  ( ( R e. CRing /\ s e. B /\ t e. B ) -> ( ( s .x. t ) e. U <-> ( s e. U /\ t e. U ) ) )
63 62 simplbda 
 |-  ( ( ( R e. CRing /\ s e. B /\ t e. B ) /\ ( s .x. t ) e. U ) -> t e. U )
64 40 41 42 61 63 syl31anc 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> t e. U )
65 oveq1 
 |-  ( u = t -> ( u .x. X ) = ( t .x. X ) )
66 65 eqeq1d 
 |-  ( u = t -> ( ( u .x. X ) = Y <-> ( t .x. X ) = Y ) )
67 66 adantl 
 |-  ( ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) /\ u = t ) -> ( ( u .x. X ) = Y <-> ( t .x. X ) = Y ) )
68 64 67 52 rspcedvd 
 |-  ( ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) /\ X =/= ( 0g ` R ) ) -> E. u e. U ( u .x. X ) = Y )
69 36 68 pm2.61dane 
 |-  ( ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ t e. B ) /\ ( t .x. X ) = Y ) -> E. u e. U ( u .x. X ) = Y )
70 69 r19.29an 
 |-  ( ( ( ( ph /\ s e. B ) /\ ( s .x. Y ) = X ) /\ E. t e. B ( t .x. X ) = Y ) -> E. u e. U ( u .x. X ) = Y )
71 70 an32s 
 |-  ( ( ( ( ph /\ s e. B ) /\ E. t e. B ( t .x. X ) = Y ) /\ ( s .x. Y ) = X ) -> E. u e. U ( u .x. X ) = Y )
72 71 ex 
 |-  ( ( ( ph /\ s e. B ) /\ E. t e. B ( t .x. X ) = Y ) -> ( ( s .x. Y ) = X -> E. u e. U ( u .x. X ) = Y ) )
73 72 an32s 
 |-  ( ( ( ph /\ E. t e. B ( t .x. X ) = Y ) /\ s e. B ) -> ( ( s .x. Y ) = X -> E. u e. U ( u .x. X ) = Y ) )
74 73 imp 
 |-  ( ( ( ( ph /\ E. t e. B ( t .x. X ) = Y ) /\ s e. B ) /\ ( s .x. Y ) = X ) -> E. u e. U ( u .x. X ) = Y )
75 74 r19.29an 
 |-  ( ( ( ph /\ E. t e. B ( t .x. X ) = Y ) /\ E. s e. B ( s .x. Y ) = X ) -> E. u e. U ( u .x. X ) = Y )
76 75 anasss 
 |-  ( ( ph /\ ( E. t e. B ( t .x. X ) = Y /\ E. s e. B ( s .x. Y ) = X ) ) -> E. u e. U ( u .x. X ) = Y )
77 15 76 sylbida 
 |-  ( ( ph /\ ( X .|| Y /\ Y .|| X ) ) -> E. u e. U ( u .x. X ) = Y )
78 4 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( u .x. X ) = Y ) -> X e. B )
79 5 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( u .x. X ) = Y ) -> Y e. B )
80 16 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( u .x. X ) = Y ) -> R e. Ring )
81 simplr 
 |-  ( ( ( ph /\ u e. U ) /\ ( u .x. X ) = Y ) -> u e. U )
82 simpr 
 |-  ( ( ( ph /\ u e. U ) /\ ( u .x. X ) = Y ) -> ( u .x. X ) = Y )
83 1 2 3 78 79 6 7 80 81 82 dvdsruassoi 
 |-  ( ( ( ph /\ u e. U ) /\ ( u .x. X ) = Y ) -> ( X .|| Y /\ Y .|| X ) )
84 83 r19.29an 
 |-  ( ( ph /\ E. u e. U ( u .x. X ) = Y ) -> ( X .|| Y /\ Y .|| X ) )
85 77 84 impbida 
 |-  ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> E. u e. U ( u .x. X ) = Y ) )