Metamath Proof Explorer

Theorem rprmasso

Description: In an integral domain, the associate of a prime is a prime. (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 )
rprmasso.y 
|- ( ph -> Y .|| X )
Assertion rprmasso 
|- ( ph -> Y e. P )

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 rprmasso.y 
 |-  ( ph -> Y .|| X )
8 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
9 1 2 4 5 rprmcl 
 |-  ( ph -> X e. B )
10 1 3 dvdsrcl 
 |-  ( Y .|| X -> Y e. B )
11 7 10 syl 
 |-  ( ph -> Y e. B )
12 4 idomringd 
 |-  ( ph -> R e. Ring )
13 1 8 3 9 11 12 rspsnasso 
 |-  ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> ( ( RSpan ` R ) ` { Y } ) = ( ( RSpan ` R ) ` { X } ) ) )
14 6 7 13 mpbi2and 
 |-  ( ph -> ( ( RSpan ` R ) ` { Y } ) = ( ( RSpan ` R ) ` { X } ) )
15 4 idomcringd 
 |-  ( ph -> R e. CRing )
16 5 2 eleqtrdi 
 |-  ( ph -> X e. ( RPrime ` R ) )
17 8 15 16 rsprprmprmidl 
 |-  ( ph -> ( ( RSpan ` R ) ` { X } ) e. ( PrmIdeal ` R ) )
18 14 17 eqeltrd 
 |-  ( ph -> ( ( RSpan ` R ) ` { Y } ) e. ( PrmIdeal ` R ) )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 2 19 4 5 rprmnz 
 |-  ( ph -> X =/= ( 0g ` R ) )
21 12 adantr 
 |-  ( ( ph /\ Y = ( 0g ` R ) ) -> R e. Ring )
22 9 adantr 
 |-  ( ( ph /\ Y = ( 0g ` R ) ) -> X e. B )
23 simpr 
 |-  ( ( ph /\ Y = ( 0g ` R ) ) -> Y = ( 0g ` R ) )
24 7 adantr 
 |-  ( ( ph /\ Y = ( 0g ` R ) ) -> Y .|| X )
25 23 24 eqbrtrrd 
 |-  ( ( ph /\ Y = ( 0g ` R ) ) -> ( 0g ` R ) .|| X )
26 1 3 19 dvdsr02 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( 0g ` R ) .|| X <-> X = ( 0g ` R ) ) )
27 26 biimpa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ ( 0g ` R ) .|| X ) -> X = ( 0g ` R ) )
28 21 22 25 27 syl21anc 
 |-  ( ( ph /\ Y = ( 0g ` R ) ) -> X = ( 0g ` R ) )
29 20 28 mteqand 
 |-  ( ph -> Y =/= ( 0g ` R ) )
30 19 1 2 8 4 11 29 rsprprmprmidlb 
 |-  ( ph -> ( Y e. P <-> ( ( RSpan ` R ) ` { Y } ) e. ( PrmIdeal ` R ) ) )
31 18 30 mpbird 
 |-  ( ph -> Y e. P )