Metamath Proof Explorer

Theorem rprmirredb

Description: In a principal ideal domain, the converse of rprmirred holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmirredb.p 
|- P = ( RPrime ` R )
rprmirredb.i 
|- I = ( Irred ` R )
rprmirredb.r 
|- ( ph -> R e. PID )
Assertion rprmirredb 
|- ( ph -> I = P )

Proof

Step Hyp Ref Expression
1 rprmirredb.p 
 |-  P = ( RPrime ` R )
2 rprmirredb.i 
 |-  I = ( Irred ` R )
3 rprmirredb.r 
 |-  ( ph -> R e. PID )
4 3 adantr 
 |-  ( ( ph /\ p e. I ) -> R e. PID )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 2 5 irredcl 
 |-  ( p e. I -> p e. ( Base ` R ) )
7 6 adantl 
 |-  ( ( ph /\ p e. I ) -> p e. ( Base ` R ) )
8 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
9 2 8 irrednu 
 |-  ( p e. I -> -. p e. ( Unit ` R ) )
10 9 adantl 
 |-  ( ( ph /\ p e. I ) -> -. p e. ( Unit ` R ) )
11 df-pid 
 |-  PID = ( IDomn i^i LPIR )
12 3 11 eleqtrdi 
 |-  ( ph -> R e. ( IDomn i^i LPIR ) )
13 12 elin1d 
 |-  ( ph -> R e. IDomn )
14 13 idomringd 
 |-  ( ph -> R e. Ring )
15 14 adantr 
 |-  ( ( ph /\ p e. I ) -> R e. Ring )
16 simpr 
 |-  ( ( ph /\ p e. I ) -> p e. I )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 2 17 irredn0 
 |-  ( ( R e. Ring /\ p e. I ) -> p =/= ( 0g ` R ) )
19 15 16 18 syl2anc 
 |-  ( ( ph /\ p e. I ) -> p =/= ( 0g ` R ) )
20 nelsn 
 |-  ( p =/= ( 0g ` R ) -> -. p e. { ( 0g ` R ) } )
21 19 20 syl 
 |-  ( ( ph /\ p e. I ) -> -. p e. { ( 0g ` R ) } )
22 eqid 
 |-  ( ( Unit ` R ) u. { ( 0g ` R ) } ) = ( ( Unit ` R ) u. { ( 0g ` R ) } )
23 nelun 
 |-  ( ( ( Unit ` R ) u. { ( 0g ` R ) } ) = ( ( Unit ` R ) u. { ( 0g ` R ) } ) -> ( -. p e. ( ( Unit ` R ) u. { ( 0g ` R ) } ) <-> ( -. p e. ( Unit ` R ) /\ -. p e. { ( 0g ` R ) } ) ) )
24 22 23 ax-mp 
 |-  ( -. p e. ( ( Unit ` R ) u. { ( 0g ` R ) } ) <-> ( -. p e. ( Unit ` R ) /\ -. p e. { ( 0g ` R ) } ) )
25 10 21 24 sylanbrc 
 |-  ( ( ph /\ p e. I ) -> -. p e. ( ( Unit ` R ) u. { ( 0g ` R ) } ) )
26 7 25 eldifd 
 |-  ( ( ph /\ p e. I ) -> p e. ( ( Base ` R ) \ ( ( Unit ` R ) u. { ( 0g ` R ) } ) ) )
27 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
28 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
29 15 ad3antrrr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. Ring )
30 7 ad3antrrr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> p e. ( Base ` R ) )
31 5 27 28 29 30 ellpi 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( ( RSpan ` R ) ` { p } ) <-> p ( ||r ` R ) x ) )
32 31 biimpa 
 |-  ( ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ x e. ( ( RSpan ` R ) ` { p } ) ) -> p ( ||r ` R ) x )
33 5 27 28 29 30 ellpi 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( y e. ( ( RSpan ` R ) ` { p } ) <-> p ( ||r ` R ) y ) )
34 33 biimpa 
 |-  ( ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ y e. ( ( RSpan ` R ) ` { p } ) ) -> p ( ||r ` R ) y )
35 13 idomcringd 
 |-  ( ph -> R e. CRing )
36 35 ad4antr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. CRing )
37 2 eleq2i 
 |-  ( p e. I <-> p e. ( Irred ` R ) )
38 37 biimpi 
 |-  ( p e. I -> p e. ( Irred ` R ) )
39 38 adantl 
 |-  ( ( ph /\ p e. I ) -> p e. ( Irred ` R ) )
40 eqid 
 |-  ( ( RSpan ` R ) ` { p } ) = ( ( RSpan ` R ) ` { p } )
41 7 snssd 
 |-  ( ( ph /\ p e. I ) -> { p } C_ ( Base ` R ) )
42 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
43 27 5 42 rspcl 
 |-  ( ( R e. Ring /\ { p } C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( LIdeal ` R ) )
44 15 41 43 syl2anc 
 |-  ( ( ph /\ p e. I ) -> ( ( RSpan ` R ) ` { p } ) e. ( LIdeal ` R ) )
45 5 27 17 40 4 7 19 44 mxidlirred 
 |-  ( ( ph /\ p e. I ) -> ( ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) <-> p e. ( Irred ` R ) ) )
46 39 45 mpbird 
 |-  ( ( ph /\ p e. I ) -> ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) )
47 46 ad3antrrr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) )
48 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
49 48 mxidlprm 
 |-  ( ( R e. CRing /\ ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) )
50 36 47 49 syl2anc 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) )
51 simpllr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> x e. ( Base ` R ) )
52 simplr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> y e. ( Base ` R ) )
53 simpr 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> p ( ||r ` R ) ( x ( .r ` R ) y ) )
54 5 27 28 29 30 ellpi 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( ( x ( .r ` R ) y ) e. ( ( RSpan ` R ) ` { p } ) <-> p ( ||r ` R ) ( x ( .r ` R ) y ) ) )
55 53 54 mpbird 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) e. ( ( RSpan ` R ) ` { p } ) )
56 eqid 
 |-  ( .r ` R ) = ( .r ` R )
57 5 56 prmidlc 
 |-  ( ( ( R e. CRing /\ ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ ( x ( .r ` R ) y ) e. ( ( RSpan ` R ) ` { p } ) ) ) -> ( x e. ( ( RSpan ` R ) ` { p } ) \/ y e. ( ( RSpan ` R ) ` { p } ) ) )
58 36 50 51 52 55 57 syl23anc 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( ( RSpan ` R ) ` { p } ) \/ y e. ( ( RSpan ` R ) ` { p } ) ) )
59 32 34 58 orim12da 
 |-  ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( p ( ||r ` R ) x \/ p ( ||r ` R ) y ) )
60 59 ex 
 |-  ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( p ( ||r ` R ) ( x ( .r ` R ) y ) -> ( p ( ||r ` R ) x \/ p ( ||r ` R ) y ) ) )
61 60 anasss 
 |-  ( ( ( ph /\ p e. I ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( p ( ||r ` R ) ( x ( .r ` R ) y ) -> ( p ( ||r ` R ) x \/ p ( ||r ` R ) y ) ) )
62 61 ralrimivva 
 |-  ( ( ph /\ p e. I ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( p ( ||r ` R ) ( x ( .r ` R ) y ) -> ( p ( ||r ` R ) x \/ p ( ||r ` R ) y ) ) )
63 5 8 17 28 56 isrprm 
 |-  ( R e. PID -> ( p e. ( RPrime ` R ) <-> ( p e. ( ( Base ` R ) \ ( ( Unit ` R ) u. { ( 0g ` R ) } ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( p ( ||r ` R ) ( x ( .r ` R ) y ) -> ( p ( ||r ` R ) x \/ p ( ||r ` R ) y ) ) ) ) )
64 63 biimpar 
 |-  ( ( R e. PID /\ ( p e. ( ( Base ` R ) \ ( ( Unit ` R ) u. { ( 0g ` R ) } ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( p ( ||r ` R ) ( x ( .r ` R ) y ) -> ( p ( ||r ` R ) x \/ p ( ||r ` R ) y ) ) ) ) -> p e. ( RPrime ` R ) )
65 4 26 62 64 syl12anc 
 |-  ( ( ph /\ p e. I ) -> p e. ( RPrime ` R ) )
66 65 1 eleqtrrdi 
 |-  ( ( ph /\ p e. I ) -> p e. P )
67 simpr 
 |-  ( ( ph /\ p e. P ) -> p e. P )
68 13 adantr 
 |-  ( ( ph /\ p e. P ) -> R e. IDomn )
69 1 2 67 68 rprmirred 
 |-  ( ( ph /\ p e. P ) -> p e. I )
70 66 69 impbida 
 |-  ( ph -> ( p e. I <-> p e. P ) )
71 70 eqrdv 
 |-  ( ph -> I = P )