Metamath Proof Explorer

Theorem rprmasso2

Description: In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmasso.b 
|- B = ( Base ` R )
rprmasso.p 
|- P = ( RPrime ` R )
rprmasso.d 
|- .|| = ( ||r ` R )
rprmasso.r 
|- ( ph -> R e. IDomn )
rprmasso.x 
|- ( ph -> X e. P )
rprmasso.1 
|- ( ph -> X .|| Y )
rprmasso2.y 
|- ( ph -> Y e. P )
Assertion rprmasso2 
|- ( ph -> Y .|| X )

Proof

Step Hyp Ref Expression
1 rprmasso.b 
 |-  B = ( Base ` R )
2 rprmasso.p 
 |-  P = ( RPrime ` R )
3 rprmasso.d 
 |-  .|| = ( ||r ` R )
4 rprmasso.r 
 |-  ( ph -> R e. IDomn )
5 rprmasso.x 
 |-  ( ph -> X e. P )
6 rprmasso.1 
 |-  ( ph -> X .|| Y )
7 rprmasso2.y 
 |-  ( ph -> Y e. P )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 4 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> R e. IDomn )
10 7 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> Y e. P )
11 simplr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> t e. B )
12 1 2 4 5 rprmcl 
 |-  ( ph -> X e. B )
13 12 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> X e. B )
14 4 idomringd 
 |-  ( ph -> R e. Ring )
15 1 2 4 7 rprmcl 
 |-  ( ph -> Y e. B )
16 1 3 dvdsrid 
 |-  ( ( R e. Ring /\ Y e. B ) -> Y .|| Y )
17 14 15 16 syl2anc 
 |-  ( ph -> Y .|| Y )
18 17 ad2antrr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> Y .|| Y )
19 simpr 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> ( t ( .r ` R ) X ) = Y )
20 18 19 breqtrrd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> Y .|| ( t ( .r ` R ) X ) )
21 1 2 3 8 9 10 11 13 20 rprmdvds 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> ( Y .|| t \/ Y .|| X ) )
22 12 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> X e. B )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 11 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> t e. B )
25 simpr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> t = ( 0g ` R ) )
26 25 oveq1d 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> ( t ( .r ` R ) X ) = ( ( 0g ` R ) ( .r ` R ) X ) )
27 simplr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> ( t ( .r ` R ) X ) = Y )
28 1 8 23 14 12 ringlzd 
 |-  ( ph -> ( ( 0g ` R ) ( .r ` R ) X ) = ( 0g ` R ) )
29 28 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) X ) = ( 0g ` R ) )
30 26 27 29 3eqtr3d 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> Y = ( 0g ` R ) )
31 2 23 4 7 rprmnz 
 |-  ( ph -> Y =/= ( 0g ` R ) )
32 31 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> Y =/= ( 0g ` R ) )
33 32 neneqd 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ t = ( 0g ` R ) ) -> -. Y = ( 0g ` R ) )
34 30 33 pm2.65da 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> -. t = ( 0g ` R ) )
35 34 neqned 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> t =/= ( 0g ` R ) )
36 35 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> t =/= ( 0g ` R ) )
37 24 36 eldifsnd 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> t e. ( B \ { ( 0g ` R ) } ) )
38 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> R e. Ring )
39 simplr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> u e. B )
40 13 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> X e. B )
41 1 8 38 39 40 ringcld 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( u ( .r ` R ) X ) e. B )
42 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
43 1 42 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
44 14 43 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
45 44 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( 1r ` R ) e. B )
46 4 idomdomd 
 |-  ( ph -> R e. Domn )
47 46 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> R e. Domn )
48 19 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( t ( .r ` R ) X ) = Y )
49 48 oveq2d 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( u ( .r ` R ) ( t ( .r ` R ) X ) ) = ( u ( .r ` R ) Y ) )
50 simpr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( u ( .r ` R ) Y ) = t )
51 49 50 eqtrd 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( u ( .r ` R ) ( t ( .r ` R ) X ) ) = t )
52 4 idomcringd 
 |-  ( ph -> R e. CRing )
53 52 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> R e. CRing )
54 1 8 53 24 39 40 crng12d 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( t ( .r ` R ) ( u ( .r ` R ) X ) ) = ( u ( .r ` R ) ( t ( .r ` R ) X ) ) )
55 1 8 42 38 24 ringridmd 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( t ( .r ` R ) ( 1r ` R ) ) = t )
56 51 54 55 3eqtr4d 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( t ( .r ` R ) ( u ( .r ` R ) X ) ) = ( t ( .r ` R ) ( 1r ` R ) ) )
57 1 23 8 37 41 45 47 56 domnlcan 
 |-  ( ( ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) /\ u e. B ) /\ ( u ( .r ` R ) Y ) = t ) -> ( u ( .r ` R ) X ) = ( 1r ` R ) )
58 15 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> Y e. B )
59 simpr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> Y .|| t )
60 1 3 8 dvdsr2 
 |-  ( Y e. B -> ( Y .|| t <-> E. u e. B ( u ( .r ` R ) Y ) = t ) )
61 60 biimpa 
 |-  ( ( Y e. B /\ Y .|| t ) -> E. u e. B ( u ( .r ` R ) Y ) = t )
62 58 59 61 syl2anc 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> E. u e. B ( u ( .r ` R ) Y ) = t )
63 57 62 reximddv3 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> E. u e. B ( u ( .r ` R ) X ) = ( 1r ` R ) )
64 1 3 8 dvdsr2 
 |-  ( X e. B -> ( X .|| ( 1r ` R ) <-> E. u e. B ( u ( .r ` R ) X ) = ( 1r ` R ) ) )
65 64 biimpar 
 |-  ( ( X e. B /\ E. u e. B ( u ( .r ` R ) X ) = ( 1r ` R ) ) -> X .|| ( 1r ` R ) )
66 22 63 65 syl2anc 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> X .|| ( 1r ` R ) )
67 42 3 2 52 5 rprmndvdsr1 
 |-  ( ph -> -. X .|| ( 1r ` R ) )
68 67 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) /\ Y .|| t ) -> -. X .|| ( 1r ` R ) )
69 66 68 pm2.65da 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> -. Y .|| t )
70 21 69 orcnd 
 |-  ( ( ( ph /\ t e. B ) /\ ( t ( .r ` R ) X ) = Y ) -> Y .|| X )
71 1 3 8 dvdsr 
 |-  ( X .|| Y <-> ( X e. B /\ E. t e. B ( t ( .r ` R ) X ) = Y ) )
72 6 71 sylib 
 |-  ( ph -> ( X e. B /\ E. t e. B ( t ( .r ` R ) X ) = Y ) )
73 72 simprd 
 |-  ( ph -> E. t e. B ( t ( .r ` R ) X ) = Y )
74 70 73 r19.29a 
 |-  ( ph -> Y .|| X )