Metamath Proof Explorer

Theorem rsprprmprmidlb

Description: In an integral domain, an ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rsprprmprmidlb.0 
|- .0. = ( 0g ` R )
rsprprmprmidlb.b 
|- B = ( Base ` R )
rsprprmprmidlb.p 
|- P = ( RPrime ` R )
rsprprmprmidlb.k 
|- K = ( RSpan ` R )
rsprprmprmidlb.r 
|- ( ph -> R e. IDomn )
rsprprmprmidlb.x 
|- ( ph -> X e. B )
rsprprmprmidlb.1 
|- ( ph -> X =/= .0. )
Assertion rsprprmprmidlb 
|- ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) )

Proof

Step Hyp Ref Expression
1 rsprprmprmidlb.0 
 |-  .0. = ( 0g ` R )
2 rsprprmprmidlb.b 
 |-  B = ( Base ` R )
3 rsprprmprmidlb.p 
 |-  P = ( RPrime ` R )
4 rsprprmprmidlb.k 
 |-  K = ( RSpan ` R )
5 rsprprmprmidlb.r 
 |-  ( ph -> R e. IDomn )
6 rsprprmprmidlb.x 
 |-  ( ph -> X e. B )
7 rsprprmprmidlb.1 
 |-  ( ph -> X =/= .0. )
8 5 idomcringd 
 |-  ( ph -> R e. CRing )
9 8 adantr 
 |-  ( ( ph /\ X e. P ) -> R e. CRing )
10 3 a1i 
 |-  ( ph -> P = ( RPrime ` R ) )
11 10 eleq2d 
 |-  ( ph -> ( X e. P <-> X e. ( RPrime ` R ) ) )
12 11 biimpa 
 |-  ( ( ph /\ X e. P ) -> X e. ( RPrime ` R ) )
13 4 9 12 rsprprmprmidl 
 |-  ( ( ph /\ X e. P ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) )
14 5 adantr 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. IDomn )
15 6 adantr 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. B )
16 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
17 eqid 
 |-  ( K ` { X } ) = ( K ` { X } )
18 16 4 17 2 15 14 unitpidl1 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( ( K ` { X } ) = B <-> X e. ( Unit ` R ) ) )
19 18 biimpar 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) = B )
20 14 idomringd 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. Ring )
21 eqid 
 |-  ( .r ` R ) = ( .r ` R )
22 2 21 prmidlnr 
 |-  ( ( R e. Ring /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B )
23 20 22 sylancom 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B )
24 23 adantr 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) =/= B )
25 24 neneqd 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> -. ( K ` { X } ) = B )
26 19 25 pm2.65da 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( Unit ` R ) )
27 nelsn 
 |-  ( X =/= .0. -> -. X e. { .0. } )
28 7 27 syl 
 |-  ( ph -> -. X e. { .0. } )
29 28 adantr 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. { .0. } )
30 eqid 
 |-  ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } )
31 nelun 
 |-  ( ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } ) -> ( -. X e. ( ( Unit ` R ) u. { .0. } ) <-> ( -. X e. ( Unit ` R ) /\ -. X e. { .0. } ) ) )
32 30 31 ax-mp 
 |-  ( -. X e. ( ( Unit ` R ) u. { .0. } ) <-> ( -. X e. ( Unit ` R ) /\ -. X e. { .0. } ) )
33 26 29 32 sylanbrc 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( ( Unit ` R ) u. { .0. } ) )
34 15 33 eldifd 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) )
35 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
36 20 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. Ring )
37 6 ad4antr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> X e. B )
38 2 4 35 36 37 ellpi 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) <-> X ( ||r ` R ) x ) )
39 38 biimpa 
 |-  ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ x e. ( K ` { X } ) ) -> X ( ||r ` R ) x )
40 2 4 35 36 37 ellpi 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( y e. ( K ` { X } ) <-> X ( ||r ` R ) y ) )
41 40 biimpa 
 |-  ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ y e. ( K ` { X } ) ) -> X ( ||r ` R ) y )
42 8 ad4antr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. CRing )
43 simp-4r 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) )
44 simpllr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> x e. B )
45 simplr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> y e. B )
46 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> R e. Ring )
47 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> X e. B )
48 2 4 35 46 47 ellpi 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` R ) y ) e. ( K ` { X } ) <-> X ( ||r ` R ) ( x ( .r ` R ) y ) ) )
49 48 biimpar 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) e. ( K ` { X } ) )
50 2 21 prmidlc 
 |-  ( ( ( R e. CRing /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B /\ ( x ( .r ` R ) y ) e. ( K ` { X } ) ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) )
51 42 43 44 45 49 50 syl23anc 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) )
52 39 41 51 orim12da 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) )
53 52 ex 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) )
54 53 anasss 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) )
55 54 ralrimivva 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) )
56 2 16 1 35 21 isrprm 
 |-  ( R e. IDomn -> ( X e. ( RPrime ` R ) <-> ( X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) /\ A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) ) )
57 56 biimpar 
 |-  ( ( R e. IDomn /\ ( X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) /\ A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) ) -> X e. ( RPrime ` R ) )
58 14 34 55 57 syl12anc 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( RPrime ` R ) )
59 58 3 eleqtrrdi 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. P )
60 13 59 impbida 
 |-  ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) )